Extracting information from resolution proof trees

DOI10.1016/0004-3702(71)90003-8MaRDI QIDQ2547494zbMATH OpenOpenAlexFDO

Authors David C. Luckham, Nils J. Nilsson

Publication date 1971

Published in Artificial Intelligence (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0004-3702(71)90003-8

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Cites work

• A Machine-Oriented Logic Based on the Resolution Principle
• scientific article; zbMATH DE number 3236046 (Why is no real title available?)
• scientific article; zbMATH DE number 3343519 (Why is no real title available?)
• scientific article; zbMATH DE number 3380160 (Why is no real title available?)
• Resolution With Merging

Cited in

(12)

• A complete, nonredundant algorithm for reversed Skolemization
• A logic for default reasoning
• \(\Pi\)-representation: A clause representation for parallel search
• A logical theory of robot problem solving
• Constructing specification morphisms
• Rule-oriented methods in problem solving
• Formal methods in the design of question-answering systems
• Book review of: S. Russell and P. Norvig, Artificial intelligence: a modern approach
• A note on answer extraction in resolution-based systems
• Representations of the language recognition problem for a theorem prover
• Defining answer classes using resolution refutation
• Un-Skolemizing clause sets

This page was built for publication: Extracting information from resolution proof trees

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