A new combination of input and unit deductions for Horn sentences

DOI10.1016/0020-0190(84)90113-3zbMath0563.68072OpenAlexW2010308603MaRDI QIDQ1057665

Shuji Doshita, Susumu Yamasaki, Mikio Yoshida, Mikito Hirata

Publication date: 1984

Published in: Information Processing Letters (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0020-0190(84)90113-3

zbMATH Keywords

Horn clausesresolutionlogic programminginput refutation

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) General topics in the theory of software (68N01)

Related Items

A fixpoint semantics of Horn sentences based on substitution sets, Automatic theorem proving. II

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The Semantics of Predicate Logic as a Programming Language
• Horn clause computability
• The Specialization of Programs by Theorem Proving