Ordered semantic hyper-linking

DOI10.1023/A:1006376231563MaRDI QIDQ1581853zbMATH OpenOpenAlexFDO

Authors Yunshan Zhu, David A. Plaisted

Publication date 6 February 2001

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1023/a:1006376231563

zbMATH Keywords

ordered semantic hyper-linking

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Semantically guided first-order theorem proving using hyper-linking
• Eliminating dublication with the hyper-linking strategy
• Semantic tableaux with ordering restrictions
• Automated Reasoning with Analytic Tableaux and Related Methods
• The search efficiency of theorem proving strategies

Cited in

(24)

• Set of support, demodulation, paramodulation: a historical perspective
• SCL(EQ): SCL for first-order logic with equality
• SCL(EQ): SCL for first-order logic with equality
• The Relative Power of Semantics and Unification
• Semantically-guided goal-sensitive reasoning: inference system and completeness
• Semantically-guided goal-sensitive reasoning: model representation
• Visualizing SAT instances and runs of the DPLL algorithm
• A combined superposition and model evolution calculus
• An instantiation scheme for satisfiability modulo theories
• Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover
• Comparing instance generation methods for automated reasoning
• Semantically guided first-order theorem proving using hyper-linking
• Solving quantified verification conditions using satisfiability modulo theories
• The disconnection tableau calculus
• On First-Order Model-Based Reasoning
• Automated Reasoning with Analytic Tableaux and Related Methods
• Model evolution with equality -- revised and implemented
• Inst-Gen -- a modular approach to instantiation-based automated reasoning
• Modular instantiation schemes
• The model evolution calculus as a first-order DPLL method
• Towards a unified model of search in theorem-proving: subgoal-reduction strategies
• History and prospects for first-order automated deduction
• Soft typing for ordered resolution
• A relevance restriction strategy for automated deduction

Describes a project that uses

Uses Software

• SATCHMO

This page was built for publication: Ordered semantic hyper-linking

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