More on trees and finite satisfiability: The taming of terms (Q1098832)

From MaRDI portal





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
    0 references
    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

    Identifiers