Is there any software around that using the Fitch format (used in Language, Proof and Logic), allows one to put a specific set of premises and goals and have it show us the full list of steps needed to solve the problem?
Fitch Format Proofs - Any automatic solvers around? [closed]
Asked Answered
Short answer: No.
Medium Answer: Can't really be done, though one could write a program to check the validity of a given proof fairly easily. In the case of propositional logic, the problem of automatically finding a proof is NP-complete (though it is decidable!), and in first order logic there are true theorems for which the prover would never stop. (undecidable) (via Gödel's incompleteness proof)
If you're interested in writing such a thing, you can take a stab at it, and maybe get it to work for some smaller cases, but it's not doable in general.
If you're looking for such a thing to get answers for your homework, quit trying. (a) you won't find it and (b) the problems from that book are pretty easy, and can be fun! Just give them a try, and seek out help if needed. and, of course, (c) you won't learn anything if you cheat.
Actually there are mechanical ways of generating Fitch style proofs. E.g. chapter 13 of Paul Teller's logic textbook contains a description of such a procedure for propositional logic (basically truth trees in Fitch notation). Also, first order logic is semidecidable, meaning there are ways to mechanically find a proof if the sequent is valid (though the search may never terminate in the case of an invalid sequent). Of course none of this is of help for logic homework, since such proofs tend to be ridiculously long ;-) –
Rosecan
Short answer: No.
Medium Answer: Can't really be done, though one could write a program to check the validity of a given proof fairly easily. In the case of propositional logic, the problem of automatically finding a proof is NP-complete (though it is decidable!), and in first order logic there are true theorems for which the prover would never stop. (undecidable) (via Gödel's incompleteness proof)
If you're interested in writing such a thing, you can take a stab at it, and maybe get it to work for some smaller cases, but it's not doable in general.
If you're looking for such a thing to get answers for your homework, quit trying. (a) you won't find it and (b) the problems from that book are pretty easy, and can be fun! Just give them a try, and seek out help if needed. and, of course, (c) you won't learn anything if you cheat.
Actually there are mechanical ways of generating Fitch style proofs. E.g. chapter 13 of Paul Teller's logic textbook contains a description of such a procedure for propositional logic (basically truth trees in Fitch notation). Also, first order logic is semidecidable, meaning there are ways to mechanically find a proof if the sequent is valid (though the search may never terminate in the case of an invalid sequent). Of course none of this is of help for logic homework, since such proofs tend to be ridiculously long ;-) –
Rosecan
Consider Apros by OLI Carnegie Mellon http://www.phil.cmu.edu/projects/apros/ .
While this link may answer the question, it is better to include the essential parts of the answer here and provide the link for reference. Link-only answers can become invalid if the linked page changes. –
Affairs
I tried both ProofLab and LogicLab on Windows for different versions - large 32-bit executables that do not even load.. I terminated the processes after a few minutes of waiting. –
Errantry
© 2022 - 2024 — McMap. All rights reserved.