Napredna pretraga

Pregled bibliografske jedinice broj: 844300

On Satisfiability Trees


Maretić, Marcel
On Satisfiability Trees // International Journal of Applied Mathematics, 29 (2016), 5; 569-582 doi:10.12732/ijam.v29i5.5 (podatak o recenziji nije dostupan, članak, znanstveni)


Naslov
On Satisfiability Trees

Autori
Maretić, Marcel

Izvornik
International Journal of Applied Mathematics (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


Ustanove
Fakultet organizacije i informatike, Varaždin

Autor s matičnim brojem:
Marcel Maretić, (253492)

Časopis indeksira:


  • Scopus


Uključenost u ostale bibliografske baze podataka:


  • MathSciNet
  • Zentrallblatt für Mathematik/Mathematical Abstracts


Citati