Abstract

We define a satisfiability tree in the context of classical propositional logic. Satisfiability tree is a structure inspired by the Beth's semantic tableau, later refined into its modern variant by Lis and Smullyan and by the notion that tableau is a tree-like representation of a formula. Basic notions and simple graph operations that correspond to logical operators are defined for satisfiability trees. Relation to tableau, parsing trees are investigated. Clausal satisfiability trees are defined as a class of satisfiability trees suited for formulas in clausal form. Issues related to size of clausal satisfiability trees are investigated. Non-redundant clausal satisfiability trees are shown to be a simple rewrite of Robinson's refutation trees.

Citation details of the article

Journal: International Journal of Applied Mathematics
Journal ISSN (Print): ISSN 1311-1728
Journal ISSN (Electronic): ISSN 1314-8060
Volume: 29
Issue: 5
Year: 2016

DOI: 10.12732/ijam.v29i5.5

Download Section

Download the full text of article from here.

You will need Adobe Acrobat reader. For more information and free download of the reader, please follow this link.

References

1. [1] M. Ben-Ari, Mathematical Logic for Computer Science, Springer, London (2012).
2. [2] M. D’Agostino, D.M. Gabbay, R. Hahnle, J. Posegga, Handbook of Tableau Methods, Springer, Netherlands (2013).
3. [3] M. Fitting, First-Order Logic and Automated Theorem Proving, Graduate Texts in Computer Science, Springer, New York (1996).
4. [4] M. Fitting, Proof Methods for Modal and Intuitionistic Logics, Synthese Library. Springer, Netherlands (2013).
5. [5] J. A. Robinson, A machine-oriented logic based on the resolution principle, J. ACM, 12, No 1 (Jan. 1965), 23–41.
6. [6] R.M. Smullyan, First-order Logic, Dover Books on Advanced Mathematics. Dover (1995).