A relevance restriction strategy for automated deduction
From MaRDI portal
Publication:814429
DOI10.1016/S0004-3702(02)00368-5zbMath1079.68093MaRDI QIDQ814429
Adnan Yahya, David Alan Plaisted
Publication date: 7 February 2006
Published in: Artificial Intelligence (Search for Journal in Brave)
03B35: Mechanization of proofs and logical operations
Related Items
Lightweight relevance filtering for machine-generated resolution problems, SATCHMOREBID: SATCHMO(RE) with BIDirectional relevancy, MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance
Uses Software
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