Resolution graphs

DOI10.1016/0004-3702(70)90011-1MaRDI QIDQ2543000zbMATH OpenOpenAlexFDO

Authors Robert Yates, B. Raphael, T. P. Hart

Publication date 1970

Published in Artificial Intelligence (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0004-3702(70)90011-1

Mathematics Subject Classification ID

Graph theory (including graph drawing) in computer science (68R10)

Cites work

• A Linear Format for Resolution With Merging and a New Technique for Establishing Completeness
• A Machine-Oriented Logic Based on the Resolution Principle
• Automatic Theorem Proving With Renamable and Semantic Resolution
• Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
• scientific article; zbMATH DE number 3219316 (Why is no real title available?)
• scientific article; zbMATH DE number 3278281 (Why is no real title available?)
• scientific article; zbMATH DE number 3313862 (Why is no real title available?)
• scientific article; zbMATH DE number 3320385 (Why is no real title available?)
• scientific article; zbMATH DE number 3343519 (Why is no real title available?)
• scientific article; zbMATH DE number 3346109 (Why is no real title available?)
• Resolution With Merging
• Semi-Automated Mathematics
• The Concept of Demodulation in Theorem Proving
• Theorem Proving by Covering Expressions

Cited in

(6)

• Using rewriting rules for connection graphs to prove theorems
• Refutation graphs
• Paramodulated connection graphs
• Linear resolution with selection function
• A note on linear resolution strategies in consequence-finding
• Exploiting resolution-based representations for MaxSAT solving

This page was built for publication: Resolution graphs

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