Search All of the Math Forum:
Views expressed in these public forums are not endorsed by
NCTM or The Math Forum.



Re: survey on formal proof
Posted:
Apr 24, 2013 9:19 PM


On Mar 27, 2:17 am, CharlieBoo <shymath...@gmail.com> wrote: > On Mar 19, 9:13 am, Jack Campin <bo...@purr.demon.co.uk> wrote:> I hadn't come across this before. Handy summary > > of the state of the art (as of five years ago): > > >http://www.ams.org/notices/200811/index.html > > > I don't suppose our resident wheelinventors will bother with it. > > None of the theorems exhibited are new ergo nothing is generated by > the software ? it is all input by people. > > Actual theorem proving (generating) software is what is missing. That > is not a wheel. That doesn?t even exist to this day  in what the > professors allow to be published. > > CB
I posted some Proof Finder snippets.
I've done proof by derivation, proof by counterexample working on proof by contradiction since it involves forward chaining, then will take a brief look at proof by induction.
PROOFBYCOUNTEREXAMPLE.PRO
nat(0). nat(s(X)) : nat(X).
even(0). even(s(s(X))) : even(X).
odd(s(0)). odd(s(s(X))) : odd(X).
e(A,nats) : nat(A). e(A,evens) : even(A). e(A,odds) : odd(A).
e(A, not(evens)) : e(A, odds). e(A, not(odds)) : e(A, evens).
intersects(S1,S2) : e(A,S1),e(A,S2).
not(ss( S1 , S2 )) : intersects( S1, not(S2) ).
***********************
This is just GENERIC PROOF FINDER (slightly rigged) that uses SET REASONING (spot the 3 N.S.T. definitions)
but you can ask it:
ARE ALL NUMBERS EVEN?
ARE ALL MEMBERS OF NATS MEMBERS OF EVENS?
IS NATS C EVENS?
IN PROLOG...
? not(ss(nats,evens)) .
>YES

It actually searches for the intersection of set NATS and ODDS finds s(0) , 1 and returns YES.
ANSWER: NOT ALL NATS ARE EVEN BECAUSE 1 IS A NAT AND NOT EVEN.
Herc  www.BLoCKPROLOG.com



