# Can I use some software method to solve and derive logic proofs?

For example, suppose I have this problem:

1. T
2. (T ⊃ (B ∨ M))
3. (M ⊃ H)
4. ~H

I heard there's a programming language called Prolog which can verify whether the conclusion was true or false. I would like to confirm if that is true or false news I heard?

• There may be more information at stackoverflow: stackoverflow.com/search?q=%5Bprolog%5D+proposition This link points to the prolog tag with "proposition" limiting it. – Frank Hubeny Jun 15 at 11:39
• Te above is propositional logic : truth table method is enough. – Mauro ALLEGRANZA Jun 15 at 11:51
• See Logic programming (including Prolog). – Mauro ALLEGRANZA Jun 15 at 11:52
• Thanks, is first order logic also possible to solve with logic programming? – user963241 Jun 16 at 0:02
• First order logic (predicate calculus) is in general undecidable, there is no algorithm to verify if the conclusion follows. If it does, Prolog, etc., will be able to verify it, if not, it may never (theoretically) stop. In practice, it will report failure to resolve the query, see Negation as failure. – Conifold Jun 16 at 10:21

Makoto Tsukada describes a proof checking program using Prolog. Here is the abstract:

A proof system for propositional and predicate logic is discussed. As a meta-language specifying the system, a logic programming language, namely, Prolog is adopted. All of proof rules, axioms, definitions, theorems and also proofs can be described as predicates of Prolog.

So Prolog can be used to verify whether deductions are valid or not.

Other software may be used as well that might be easier to use and require no programming. To illustrate only three of them I will take the following example from the OP:

1. T

2. (T ⊃ (B ∨ M))

3. (M ⊃ H)

4. ~H

I will assume that 4 is the desired conclusion. Then what we want to determine is whether the following is a valid deduction:

T ∧ (T ⊃ ((B ∨ M)) ∧ (M ⊃ H)) ⊃ ~H

One could put this into a truth table generator. Here is the result using Michael Rieppel's Truth Table Generator: Note that there are three rows where the valuations of the letters lead to a false (F) result in the column with red text. Because of these valuations this is not a valid deduction.

Another way to do this is through a truth tree generator. Here is the result from the Tree Proof Generator: Note that the countermodel corresponds to the third row of the truth table. Since all we need is one countermodel to claim that the deduction is not valid this may be an adequate tool to use for one's purpose.

Neither of the above two approaches require programming and they give rapid results.

Suppose however one wants to try to find a proof using natural deduction rules. There are proof checkers that will allow one to try this. One should be aware that since countermodels exist this should not be possible for this example.

Here is the start of such an attempted proof using the proof checker associated with the forallx text: It takes more work to reach a desired proof even if a valid proof exists, but this software allows one to practice using these inference rules.

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/

Rieppel, M. Truth Table Generator. https://mrieppel.net/prog/truthtable.html

Tree Proof Generator. https://www.umsu.de/logik/trees/

Tsukada, M. (2001). PROOF CHECKING USING PROLOG (Topics in Information Sciences and Applied Functional Analysis). Retrieved on June 17, 2019 from https://repository.kulib.kyoto-u.ac.jp/dspace/bitstream/2433/64661/1/1186-8.pdf

There are also various theorem provers on the Web, e.g., https://webspass.spass-prover.org/index.html