Contradiction separation based dynamic multi-clause synergized automated deduction
DOI10.1016/J.INS.2018.04.086zbMATH Open1440.03040OpenAlexW2808325100MaRDI QIDQ2198231FDOQ2198231
Authors: Yang Xu, Jun Liu, Shuwei Chen, Xiaomei Zhong, Xingxing He 
Publication date: 9 September 2020
Published in: Information Sciences (Search for Journal in Brave)
Full work available at URL: https://pure.ulster.ac.uk/ws/files/77319048/Information_Science_CS_2018_F_Accepted.pdf
Recommendations
resolutionautomated deductionfirst-order logictheorem provingpropositional logiccontradiction separationdynamic multi-clause synergized deduction
Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Cites Work
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
- MizAR 40 for Mizar 40
- System description: E 1.8
- Scavenger 0.1: a theorem prover based on conflict resolution
- Scavenger
- Title not available (Why is that?)
- A Machine-Oriented Logic Based on the Resolution Principle
- Title not available (Why is that?)
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- The 481 ways to split a clause and deal with propositional variables
- Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
- Title not available (Why is that?)
- Blocked clause elimination
- On a generalization of extended resolution
- Paramodulation-based theorem proving
- Handbook of automated reasoning. In 2 vols
- Title not available (Why is that?)
- Complexity and related enhancements for automated theorem-proving programs
- The search efficiency of theorem proving strategies
- Limited resource strategy in resolution theorem proving
- On finding short resolution refutations and small unsatisfiable subsets
- Semantically-guided goal-sensitive reasoning: inference system and completeness
- Performance of clause selection heuristics for saturation-based theorem proving
- Schubert's steamroller problem: Formulations and solutions
- A simplified way of proving trade-off results for resolution
- Another Generalization of Resolution
- Stratified resolution
- System description: E.T. 0.1
- A unifying principle for clause elimination in first-order logic
- Selecting the selection
- Super-blocked clauses
- Clause elimination for SAT and QSAT
- Abstract interpretation as automated deduction
- Detecting inconsistencies in large first-order knowledge bases
- History and prospects for first-order automated deduction
- Towards the compression of first-order resolution proofs by lowering unit clauses
- An encyclopaedia of proof systems
Cited In (6)
- On structures of regular standard contradictions in propositional logic
- \( \alpha \)-paramodulation method for a lattice-valued logic \(L_nF(X)\) with equality
- GRUNGE: a grand unified ATP challenge
- A multi-clause dynamic deduction algorithm based on standard contradiction separation rule
- A novel algorithmic construction for deductions of categorical polysyllogisms by Carroll's diagrams
- Fully reusing clause deduction algorithm based on standard contradiction separation rule
Uses Software
This page was built for publication: Contradiction separation based dynamic multi-clause synergized automated deduction
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2198231)
