12
$\begingroup$

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.

Improve this question
$\endgroup$
1
  • 1
    $\begingroup$ Here You have some "consumer test" of several proof assistants cs.ru.nl/~freek/comparison/diffs.ps.gz maybe it helps somehow... It consider of 17 different provers pointed here: cs.ru.nl/~freek/comparison/index.html $\endgroup$
    – kakaz
    Commented Feb 18, 2010 at 20:09

7 Answers 7

Reset to default
9
$\begingroup$

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.

Improve this answer
$\endgroup$
3
$\begingroup$

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.

Improve this answer
$\endgroup$
2
$\begingroup$

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.

Improve this answer
$\endgroup$
2
$\begingroup$

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.

Improve this answer
$\endgroup$
1
  • 1
    $\begingroup$ Note that you can model natural deduction inside a proof assistant based on Hilbert style if it allows (as they nearly all do) you to use meta-theorems to make new inferences. But if you care about natural deduction representations of first-order logic, Jape is probably the best fit. $\endgroup$
    – Charles Stewart
    Commented Feb 18, 2010 at 13:58
1
$\begingroup$

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

Improve this answer
$\endgroup$
1
$\begingroup$

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

Improve this answer
$\endgroup$
0
$\begingroup$

It's been a long time since I used it, but I believe Otter might be a system you'd be interested in.

My experience with Otter was through EPGY many years ago, which used a stripped-down version of Otter to teach first-order logic in a geometry course. It was easy to use, and a ton of fun - however, it's been a long time since I used it, and it's quite possible it has limitations/"features" that make it less ideal than other systems listed above, which I simply didn't encounter.

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .