Semantic trees revisited: Some new completeness results

DOI10.1007/3-540-61511-3_114zbMath1412.68222OpenAlexW1533172286MaRDI QIDQ4647548

Christian G. Fermüller

Publication date: 15 January 2019

Published in: Automated Deduction — Cade-13 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-61511-3_114

zbMATH Keywords

semantic treeground instancefailure noderestricted factoringsuccessor node

Mathematics Subject Classification ID

Uses Software

• OTTER

Cites Work

• Removing redundancy from a clause
• Reduction rules for resolution-based systems
• Resolution methods for the decision problem
• Resolution-based theorem proving for many-valued logics
• On Different Concepts of Resolution
• Resolution Strategies as Decision Procedures
• Proving refutational completeness of theorem-proving strategies
• A Machine-Oriented Logic Based on the Resolution Principle
• Automatic Theorem Proving With Renamable and Semantic Resolution
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Semantic trees revisited: Some new completeness results