Search All of the Math Forum:

Views expressed in these public forums are not endorsed by NCTM or The Math Forum.

Notice: We are no longer accepting new posts, but the forums will continue to be readable.

Topic: survey on formal proof
Replies: 2   Last Post: Apr 24, 2013 9:19 PM

 Graham Cooper Posts: 4,495 Registered: 5/20/10
Re: survey on formal proof
Posted: Apr 24, 2013 9:19 PM

On Mar 27, 2:17 am, Charlie-Boo <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 wheel-inventors 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.
>
> C-B

I posted some Proof Finder snippets.

I've done proof by derivation, proof by counter-example
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)

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