Contradiction separation based dynamic multi-clause synergized automated deduction

DOI10.1016/J.INS.2018.04.086MaRDI QIDQ2198231zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

resolutionautomated deductionfirst-order logictheorem provingpropositional logiccontradiction separationdynamic multi-clause synergized deduction

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• scientific article; zbMATH DE number 7267153
• scientific article; zbMATH DE number 3965462
• Automated deduction by theory resolution
• scientific article; zbMATH DE number 726582
• Reduction rules for resolution-based systems

Cites work

• scientific article; zbMATH DE number 5539366 (Why is no real title available?)
• scientific article; zbMATH DE number 1882060 (Why is no real title available?)
• scientific article; zbMATH DE number 3254919 (Why is no real title available?)
• scientific article; zbMATH DE number 3415409 (Why is no real title available?)
• A Machine-Oriented Logic Based on the Resolution Principle
• A simplified way of proving trade-off results for resolution
• A unifying principle for clause elimination in first-order logic
• Abstract interpretation as automated deduction
• An encyclopaedia of proof systems
• Another Generalization of Resolution
• Blocked clause elimination
• Clause elimination for SAT and QSAT
• Complexity and related enhancements for automated theorem-proving programs
• Detecting inconsistencies in large first-order knowledge bases
• Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
• Handbook of automated reasoning. In 2 vols
• History and prospects for first-order automated deduction
• Limited resource strategy in resolution theorem proving
• MizAR 40 for Mizar 40
• On a generalization of extended resolution
• On finding short resolution refutations and small unsatisfiable subsets
• Paramodulation-based theorem proving
• Performance of clause selection heuristics for saturation-based theorem proving
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• Scavenger
• Scavenger 0.1: a theorem prover based on conflict resolution
• Schubert's steamroller problem: Formulations and solutions
• Selecting the selection
• Semantically-guided goal-sensitive reasoning: inference system and completeness
• Stratified resolution
• Super-blocked clauses
• System description: E 1.8
• System description: E.T. 0.1
• The 481 ways to split a clause and deal with propositional variables
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• The search efficiency of theorem proving strategies
• Towards the compression of first-order resolution proofs by lowering unit clauses

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

Describes a project that uses

Uses Software

• Scavenger
• E Theorem Prover
• TPTP

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)