A relevance restriction strategy for automated deduction

DOI10.1016/S0004-3702(02)00368-5zbMath1079.68093OpenAlexW2009437478MaRDI QIDQ814429

Adnan Yahya, David Alan Plaisted

Publication date: 7 February 2006

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

Full work available at URL: https://doi.org/10.1016/s0004-3702(02)00368-5

zbMATH Keywords

Theorem provingRelevanceRelevance metricsSorted inference

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items

SATCHMOREBID: SATCHMO(RE) with BIDirectional relevancy, MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance, Sine Qua Non for Large Theory Reasoning, Lightweight relevance filtering for machine-generated resolution problems

Uses Software

• SATCHMO
• DCTP
• SATCHMOREBID

Cites Work

• Generating relevant models
• Theorem proving with abstraction
• Positive unit hyperresolution tableaux and their application to minimal model generation
• Ordered semantic hyper-linking
• Duality for goal-driven query processing in disjunctive deductive databases
• SATCHMOREBID: SATCHMO(RE) with BIDirectional relevancy
• SATCHMORE: SATCHMO with RElevancy
• Mechanical Theorem-Proving by Model Elimination
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item