Using resolution for deciding solvable classes and building finite models
From MaRDI portal
Publication:4560350
DOI10.1007/BFb0019355zbMath1412.68264MaRDI QIDQ4560350
Publication date: 11 December 2018
Published in: Baltic Computer Science (Search for Journal in Brave)
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