Ordered semantic hyper-linking

DOI10.1023/A:1006376231563zbMath0959.68115OpenAlexW1516218099MaRDI QIDQ1581853

Yunshan Zhu, David Alan 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)

Related Items (22)

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

Uses Software

• SATCHMO

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