A formal grammatical model of the resolution method for the propositional calculus

MaRDI QIDQ1422809zbMATH OpenFDO

Authors I. N. Anisimova, I. L. Bratchikov

Publication date 26 February 2004

Published in Vestnik St. Petersburg University. Mathematics (Search for Journal in Brave)

zbMATH Keywords

classical propositional logicHorn clausesresolution method

Mathematics Subject Classification ID

Classical propositional logic (03B05) Mechanization of proofs and logical operations (03B35)

Recommendations

• scientific article; zbMATH DE number 19146
• scientific article; zbMATH DE number 515732
• scientific article; zbMATH DE number 3978440
• Algorithms for testing the satisfiability of propositional formulae
• On the complexity of propositional calculus formulae

Cited in

(8)

• A new combination of input and unit deductions for Horn sentences
• Theory of logic programming. An elementary introduction
• The semantics of answer literals
• Refutation search for Horn sets by a subgoal-extraction method
• scientific article; zbMATH DE number 3940761 (Why is no real title available?)
• scientific article; zbMATH DE number 3957069 (Why is no real title available?)
• scientific article; zbMATH DE number 3978440 (Why is no real title available?)
• Parsing as non-Horn deduction

This page was built for publication: A formal grammatical model of the resolution method for the propositional calculus

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