Drexel dragonThe Math ForumDonate to the Math Forum



Search All of the Math Forum:

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


Math Forum » Discussions » sci.math.* » sci.math.independent

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

Advanced Search

Back to Topic List Back to Topic List Jump to Tree View Jump to Tree View  
Graham Cooper

Posts: 4,280
Registered: 5/20/10
Re: survey on formal proof
Posted: Apr 24, 2013 9:19 PM
  Click to see the message monospaced in plain text Plain Text   Click to reply to this topic Reply

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)

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



Point your RSS reader here for a feed of the latest messages in this topic.

[Privacy Policy] [Terms of Use]

© Drexel University 1994-2014. All Rights Reserved.
The Math Forum is a research and educational enterprise of the Drexel University School of Education.