Fully reusing clause deduction algorithm based on standard contradiction separation rule

Cites Work

Unnamed Item
Unnamed Item
Unnamed Item
The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
SATCHMORE: SATCHMO with RElevancy
Layered clause selection for theory reasoning (short paper)
Heterogeneous heuristic optimisation and scheduling for first-order theorem proving
Contradiction separation based dynamic multi-clause synergized automated deduction
Making theory reasoning simpler
Names are not just sound and smoke: word embeddings for axiom selection
Old or heavy? Decaying gracefully with age/weight shapes
Induction in saturation-based proof search
Faster, higher, stronger: E 2.3
GKC: a reasoning system for large knowledge bases
A unifying principle for clause elimination in first-order logic
Linear resolution with selection function
nanoCoP: A Non-clausal Connection Prover
Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving
Proof and Model Generation with Disconnection Tableaux
The TPTP World – Infrastructure for Automated Reasoning
History and Prospects for First-Order Automated Deduction
iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
Restricting backtracking in connection calculi
Theorem-Proving on the Computer
ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description)
Automated Reasoning
A Machine-Oriented Logic Based on the Resolution Principle
Automatic Theorem Proving With Renamable and Semantic Resolution
A multi-clause dynamic deduction algorithm based on standard contradiction separation rule
Automatic Deduction in an AI Geometry Book

This page was built for publication: Fully reusing clause deduction algorithm based on standard contradiction separation rule