Using resolution for deciding solvable classes and building finite models

DOI10.1007/BFB0019355MaRDI QIDQ4560350zbMATH OpenFDO

Authors Tanel Tammet

Publication date 11 December 2018

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

Full work available at URL https://doi.org/10.1007/BFB0019355

zbMATH Keywords

resolution methodfunctional termfinite domainHorn clausefinite model

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 4200168
• A calculus combining resolution and enumeration for building finite models
• Using resolution for testing modal satisfiability and building models
• Using resolution for testing modal satisfiability and building models
• Resolution and the integrality of satisfiability problems
• Publication:3485886
• Finite and $\omega $-resolvability
• \(T\)-resolution: Refinements and model elimination
• scientific article; zbMATH DE number 1534570
• On Solvable Congruences in Finitely Decidable Varieties

Cites work

• scientific article; zbMATH DE number 3122413 (Why is no real title available?)
• scientific article; zbMATH DE number 4200168 (Why is no real title available?)
• scientific article; zbMATH DE number 4104410 (Why is no real title available?)
• scientific article; zbMATH DE number 3715502 (Why is no real title available?)
• scientific article; zbMATH DE number 3441640 (Why is no real title available?)
• scientific article; zbMATH DE number 3236051 (Why is no real title available?)
• Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity
• Complexity results for classes of quantificational formulas
• Condensed detachment is complete for relevance logic: A computer-aided proof
• Maslov's inverse method and decidable classes
• On Different Concepts of Resolution
• On a bound for the complexity of terms in the resolution method
• Resolution Strategies as Decision Procedures
• The inverse method for establishing deducibility for logical calculi
• The lambda calculus, its syntax and semantics

Cited in

(11)

• Efficient model generation through compilation.
• Decision procedures using model building techniques
• Extracting models from clause sets saturated under semantic refinements of the resolution rule.
• scientific article; zbMATH DE number 515732 (Why is no real title available?)
• The search efficiency of theorem proving strategies
• Simplifying and generalizing formulae in tableaux. Pruning the search space and building models
• scientific article; zbMATH DE number 5316400 (Why is no real title available?)
• Principal numerations of functionals on admissible sets
• Working with ARMs: Complexity results on atomic representations of Herbrand models
• On compatibilities of -lock resolution method in linguistic truth-valued lattice-valued logic
• Combining enumeration and deductive techniques in order to increase the class of constructible infinite models

This page was built for publication: Using resolution for deciding solvable classes and building finite models

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4560350)