A multi-clause dynamic deduction algorithm based on standard contradiction separation rule

DOI10.1016/J.INS.2021.03.015MaRDI QIDQ6086313zbMATH OpenOpenAlexFDO

Authors Feng Cao, Yang Xu, Jun Liu, Shuwei Chen, Jianbing Yi

Publication date 9 November 2023

Published in Information Sciences (Search for Journal in Brave)

Full work available at URL https://pure.ulster.ac.uk/en/publications/0c469437-d2c5-4c87-90ae-97e03257be7b

zbMATH Keywords

ATP systemsautomated theorem provingbinary resolutionfirst-order logicS-CS dynamic deductionstandard contradiction separation

Mathematics Subject Classification ID

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

Recommendations

• Contradiction separation based dynamic multi-clause synergized automated deduction
• scientific article; zbMATH DE number 7267153
• On structures of regular standard contradictions in propositional logic
• Increasing the efficiency of automated theorem proving
• scientific article; zbMATH DE number 4033134

Cites work

• A Machine-Oriented Logic Based on the Resolution Principle
• Automated Reasoning
• Automated Reasoning
• Automatic Theorem Proving With Renamable and Semantic Resolution
• AVATAR: The Architecture for First-Order Theorem Provers
• Contradiction separation based dynamic multi-clause synergized automated deduction
• Cooperating proof attempts
• E-MaLeS 1.1
• FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover
• Fingerprint indexing for paramodulation and rewriting
• First-order automated reasoning with theories: when deduction modulo theory meets practice
• Geometric Resolution: A Proof Procedure Based on Finite Model Search
• Handbook of automated reasoning. In 2 vols
• History and prospects for first-order automated deduction
• scientific article; zbMATH DE number 5539366 (Why is no real title available?)
• scientific article; zbMATH DE number 2162299 (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 3320385 (Why is no real title available?)
• Limited resource strategy in resolution theorem proving
• Performance of clause selection heuristics for saturation-based theorem proving
• Scavenger 0.1: a theorem prover based on conflict resolution
• Selecting the selection
• Simple and Efficient Clause Subsumption with Feature Vector Indexing
• Stratified resolution
• System description: E 1.8
• System description: E.T. 0.1
• System Description: Spass Version 3.0
• The 9th IJCAR automated theorem proving system competition -- CASC-J9
• The CADE-27 automated theorem proving system competition -- CASC-27

Cited in

(2)

• On structures of regular standard contradictions in propositional logic
• Fully reusing clause deduction algorithm based on standard contradiction separation rule

This page was built for publication: A multi-clause dynamic deduction algorithm based on standard contradiction separation rule

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