For example, suppose I have this problem:
- (T ⊃ (B ∨ M))
- (M ⊃ 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?
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:
(T ⊃ (B ∨ M))
(M ⊃ 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.
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