Is there any proof assistant based on first-order logic? - MathOverflow

Is there any proof assistant based on first-order logic?

2010-02-18T10:47:12Z

I'm looking for a proof assistant in order to write formal proofs about basic facts of set theory, such as:

$a\subseteq a$
$(a,b)=(c,d)\leftrightarrow a=c\land b=d$

Natural deduction for first-order logic is the only set of rules of inference I'd like to use. Easy to install and easy to use software is preferred over more complicated one. Also, open-source software is preferred over closed-source one. No matter if the software comes with an archive of proofs that have been already formalized: I'd like to start from scratch.

Thanks.

Answer by Neel Krishnaswami for Is there any proof assistant based on first-order logic?

2010-02-18T11:24:25Z

Try Richard Bornat's Jape system. It's a teaching tool with a module for natural deduction, so there's a GUI. Proof automation is very limited, since the point is to teach people how to do formal proofs, but from the sound of your question that sounds like exactly what you want.

Answer by Ulrik Buchholtz for Is there any proof assistant based on first-order logic?

2010-02-18T16:37:15Z

You might want to search out John Harrison's book: Handbook of Practical Logic and Automated Reasoning. In the book he (among other things) develops an interactive theorem prover for first-order logic in OCaml. The code is available online.

EDIT: The system in the book is based on a Hilbert-style calculus, but due to the LCF-style of the interaction, it can be made to feel a lot like natural deduction.

Answer by Noam Zeilberger for Is there any proof assistant based on first-order logic?

2010-02-21T12:29:16Z

You could try Twelf. It is based on a more high-powered dependent type theory, but first-order logic can be encoded in a few lines (included in the examples directory), letting you write natural deduction proofs as lambda terms. You can also have a look at this short axiomatization of ZFC set theory.

Answer by vonjd for Is there any proof assistant based on first-order logic?

2010-02-22T07:32:38Z

Daniel Velleman's Proof Designer is a java applet that writes outlines of proofs in elementary set theory, under the guidance of the user. Proof Designer's approach to proof-writing is similar to the approach used in his book How to Prove it.

http://www.cs.amherst.edu/~djv/pd/pd.html

Answer by Matthew Wampler-Doty for Is there any proof assistant based on first-order logic?

2010-07-07T01:01:21Z

Isabelle supports many different logics, and it has a formulation of first order logic which you may browse here: http://isabelle.in.tum.de/dist/library/FOL/index.html. However, even though proofs are natural deduction in flavor, it does not produce anything a logician would understand as a natural deduction derivation upon shallow inspection.

The automated theorem provers Prover9, E, SPASS and Vampire are all first order systems. They do not produce proofs using natural deduction (they are all typically resolution/paramodulation based systems).

It sounds like ProofWeb is exactly like what you want. It provides a system for displaying the accompanying natural deduction/sequent calculus proof along with a computer assisted formalization. It also has a really nice interactive interface for students, and provides the possibility of assigning exercises. On the other hand, I know that it has been largely developed for Coq, which is way, way more expressive than first order logic. And even though I know that there is a development of set theory within Coq, I suspect modifying the system for basic set theory would be a nontrivial exercise.

Answer by Dan Christensen for Is there any proof assistant based on first-order logic?

2010-09-04T21:39:16Z

May I humbly suggest my DC Proof program. If is free for individual use and evaluation purposes. For more information and free, full-version download, visit my website www.dcproof.com

Dan