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

zbMATH Open1038.03518MaRDI QIDQ1422809FDOQ1422809

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

Publication date: 26 February 2004

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

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

zbMATH Keywords

classical propositional logicresolution methodHorn clauses

Mathematics Subject Classification ID

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

Cited In (7)

• Parsing as non-Horn deduction
• Refutation search for Horn sets by a subgoal-extraction method
• Title not available (Why is that?)
• Title not available (Why is that?)
• A new combination of input and unit deductions for Horn sentences
• Theory of logic programming. An elementary introduction
• Title not available (Why is that?)

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)