Using resolution for deciding solvable classes and building finite models

DOI10.1007/BFb0019355zbMath1412.68264MaRDI QIDQ4560350

Tanel Tammet

Publication date: 11 December 2018

Published in: Baltic Computer Science (Search for Journal in Brave)

zbMATH Keywords

resolution methodfunctional termfinite domainHorn clausefinite model

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Model theory of finite structures (03C13)

Related Items

On compatibilities of \(\alpha \)-lock resolution method in linguistic truth-valued lattice-valued logic ⋮ Extracting models from clause sets saturated under semantic refinements of the resolution rule. ⋮ Simplifying and generalizing formulae in tableaux. Pruning the search space and building models ⋮ Combining enumeration and deductive techniques in order to increase the class of constructible infinite models ⋮ The search efficiency of theorem proving strategies ⋮ Efficient model generation through compilation. ⋮ Working with ARMs: Complexity results on atomic representations of Herbrand models

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Maslov's inverse method and decidable classes
• The lambda calculus, its syntax and semantics
• Complexity results for classes of quantificational formulas
• Condensed detachment is complete for relevance logic: A computer-aided proof
• On a bound for the complexity of terms in the resolution method
• The inverse method for establishing deducibility for logical calculi
• On Different Concepts of Resolution
• Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity
• Resolution Strategies as Decision Procedures