Naslov
On Satisfiability Trees

Autori
Maretić, Marcel

Izvornik
International Journal of Applied Mathematics (Sofia) (1311-1728) 29 (2016), 5; 569-582

Vrsta, podvrsta i kategorija rada
Radovi u časopisima, članak, znanstveni

Ključne riječi
satisfiabilty tree ; semantic tree ; tableau ; rooted formula tree ; matching ; resolution

Sažetak
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.

Izvorni jezik
Engleski

Znanstvena područja
Matematika

POVEZANOST RADA