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

DOI10.1016/j.ins.2021.03.015zbMath1527.68257OpenAlexW3137794529MaRDI QIDQ6086313

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

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

first-order logicautomated theorem provingATP systemsbinary resolutionS-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)

Related Items (1)

On structures of regular standard contradictions in propositional logic

Cites Work

• Stratified resolution
• Limited resource strategy in resolution theorem proving
• Contradiction separation based dynamic multi-clause synergized automated deduction
• First-order automated reasoning with theories: when deduction modulo theory meets practice
• Scavenger 0.1: a theorem prover based on conflict resolution
• Selecting the Selection
• Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving
• System Description: E 1.8
• Fingerprint Indexing for Paramodulation and Rewriting
• AVATAR: The Architecture for First-Order Theorem Provers
• History and Prospects for First-Order Automated Deduction
• Cooperating Proof Attempts
• System Description: E.T. 0.1
• FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover
• System Description: Spass Version 3.0
• Geometric Resolution: A Proof Procedure Based on Finite Model Search
• Simple and Efficient Clause Subsumption with Feature Vector Indexing
• E-MaLeS 1.1
• The 9th IJCAR Automated Theorem Proving System Competition – CASC-J9
• The CADE-27 Automated theorem proving System Competition – CASC-27
• Automated Reasoning
• Automated Reasoning
• A Machine-Oriented Logic Based on the Resolution Principle
• Automatic Theorem Proving With Renamable and Semantic Resolution
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

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