Maslov's inverse method and decidable classes

DOI10.1016/0168-0072(89)90053-5zbMath0692.03009OpenAlexW1986341459MaRDI QIDQ583187

N. K. Zamov

Publication date: 1989

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0168-0072(89)90053-5

zbMATH Keywords

Maslov's inverse methodunificationresolutiondecidable classesdeducibilityextension of the clash rule

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35)

Related Items

History and Prospects for First-Order Automated Deduction, Using resolution for deciding solvable classes and building finite models, Condensed detachment is complete for relevance logic: A computer-aided proof, Decidable fragments of first-order modal logics

Cites Work

• On a bound for the complexity of terms in the resolution method
• The inverse method for establishing deducibility for logical calculi
• Resolution Strategies as Decision Procedures
• The Specialization of Programs by Theorem Proving
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item