More on trees and finite satisfiability: The taming of terms (Q1098832)
From MaRDI portal
![]() | This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use this page instead for the normal view: More on trees and finite satisfiability: The taming of terms |
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | More on trees and finite satisfiability: The taming of terms |
scientific article |
Statements
More on trees and finite satisfiability: The taming of terms (English)
0 references
1987
0 references
This note extends a result of \textit{G. Boolos} from his ``Trees and finite satisfiability: Proof of a conjecture of Burgess'' [ibid. 25, 193-197 (1984; Zbl 0561.03004)]. Boolos showed that a new rule for the existential quantifier suggested by Burgess, together with usual tableaux rules, gives a simple method of testing for finite satisfiability of first-order sentences without function symbols. The authors point out that in a first-order language with function symbols the standard tableaux rule for the universal quantifier sometimes leads to only infinite models. The authors present a tableux rule for occurrences of function symbols after all of their arguments places have been replaced with constants by use of old rules. They prove that their new rule along with the other rules dealt with by Boolos provides a test for finite satisfiability.
0 references
finite satisfiability
0 references
function symbols
0 references
tableaux
0 references