engleski

On Satisfiability Trees

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.

satisfiabilty tree ; semantic tree ; tableau ; rooted formula tree ; matching ; resolution

nije evidentirano