Reduction rules for resolution-based systems

DOI10.1016/0004-3702(91)90098-5zbMath0764.68151OpenAlexW1986619800MaRDI QIDQ1187214

Axel Präcklein, Norbert Eisinger, Hans Jürgen Ohlbach

Publication date: 28 June 1992

Published in: Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0004-3702(91)90098-5

zbMATH Keywords

reduction rulesclause graph resolution system

Mathematics Subject Classification ID

Related Items (2)

Resolution theorem proving in reified modal logics ⋮ Semantic trees revisited: Some new completeness results

Cites Work

• Matching - a special case of unification?
• Properties of substitutions and unifications
• Link inheritance in abstract clause graphs
• A new reduction rule for the connection graph proof procedure
• Using rewriting rules for connection graphs to prove theorems
• Paramodulated connection graphs
• Automated deduction by theory resolution
• Linear resolution with selection function
• Z-Resolution: Theorem-Proving with Compiled Axioms
• On the efficiency of subsumption algorithms
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• On Matrices with Connections
• A Search Technique for Clause Interconnectivity Graphs
• A Proof Procedure Using Connection Graphs
• A Machine-Oriented Logic Based on the Resolution Principle
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Reduction rules for resolution-based systems