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 method; functional term; finite domain; Horn clause; finite model

Mathematics Subject Classification ID

03B35: Mechanization of proofs and logical operations

03C13: Model theory of finite structures

Related Items

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

Cites Work

• 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
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item