Propositional calculus proving methods in Prolog. (English) Zbl 0792.68165

Summary: Two methods of proving the theorems of the propositional calculus are described in this paper – Wang’s algorithm and the method of analytical tables. Two programs in Prolog are quotated to Wang’s algorithm, for the method of analytical tables author’s program is presented. Efficiency of the programs is demonstrated on examples. Further, the practical and didactic value of presented methods and programs is discussed.


68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B35 Mechanization of proofs and logical operations
Full Text: EuDML


[1] Coelho H., Cotta J.C., Pereira L.M.: How to solve it with Prolog. Lisboa, LNEC 1985.
[2] Coelho H., Cotta J.C.: Prolog by example. Springer-Verlag 1988. · Zbl 0649.68004
[3] Smullyan R.M.: First order logic. Bratislava, ALFA 1979. · Zbl 0172.28901
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.