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 logicresolution methodHorn clauses

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

(7)

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

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)