A relevance restriction strategy for automated deduction

DOI10.1016/S0004-3702(02)00368-5MaRDI QIDQ814429zbMATH OpenOpenAlexFDO

Authors Adnan Yahya, David A. 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

RelevanceRelevance metricsSorted inferenceTheorem proving

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• scientific article; zbMATH DE number 1341620
• Lightweight relevance filtering for machine-generated resolution problems
• The search efficiency of theorem proving strategies
• Relevancy-based use of lemmas in connection tableau calculi (Diss., TU München, 1999)
• scientific article; zbMATH DE number 1037485

Cites work

• Duality for goal-driven query processing in disjunctive deductive databases
• Generating relevant models
• scientific article; zbMATH DE number 1614697 (Why is no real title available?)
• scientific article; zbMATH DE number 3872640 (Why is no real title available?)
• scientific article; zbMATH DE number 4094866 (Why is no real title available?)
• scientific article; zbMATH DE number 3568056 (Why is no real title available?)
• scientific article; zbMATH DE number 1303349 (Why is no real title available?)
• scientific article; zbMATH DE number 1341620 (Why is no real title available?)
• scientific article; zbMATH DE number 1936671 (Why is no real title available?)
• scientific article; zbMATH DE number 1765683 (Why is no real title available?)
• scientific article; zbMATH DE number 789391 (Why is no real title available?)
• scientific article; zbMATH DE number 3415409 (Why is no real title available?)
• Mechanical Theorem-Proving by Model Elimination
• Ordered semantic hyper-linking
• Positive unit hyperresolution tableaux and their application to minimal model generation
• SATCHMORE: SATCHMO with RElevancy
• SATCHMOREBID: SATCHMO(RE) with BIDirectional relevancy
• Theorem proving in large theories
• Theorem proving with abstraction

Cited in

(13)

• Lightweight relevance filtering for machine-generated resolution problems
• SATCHMOREBID: SATCHMO(RE) with BIDirectional relevancy
• Generalized completeness for SOS resolution and its application to a new notion of relevance
• Unprovability results for clause set cycles
• Relevancy-based use of lemmas in connection tableau calculi (Diss., TU München, 1999)
• MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance
• SRASS - A Semantic Relevance Axiom Selection System
• scientific article; zbMATH DE number 1303349 (Why is no real title available?)
• scientific article; zbMATH DE number 1341620 (Why is no real title available?)
• Finding theorems in NBG set theory by automated forward deduction based on strong relevant logic
• Sine qua non for large theory reasoning
• Advances in Artificial Intelligence – SBIA 2004
• The problem of finding a semantic strategy for focusing inference rules

Describes a project that uses

Uses Software

• DCTP
• SATCHMO
• SATCHMOREBID

This page was built for publication: A relevance restriction strategy for automated deduction

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