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.


  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).