A multi-clause dynamic deduction algorithm based on standard contradiction separation rule
type: Item
instance of: scholarly article
title: A multi-clause dynamic deduction algorithm based on standard contradiction separation rule
zbMATH Open document ID: 1527.68257
author: Feng Cao
author: Yang Xu
author: Jun Liu
author: Shuwei Chen
author: Jianbing Yi
published in: Information Sciences
publication date: 2023-11-09T00:00:00Z
Mathematics Subject Classification ID: 68V15
Mathematics Subject Classification ID: 03B35
zbMATH DE Number: 7763325
zbMATH Keywords: automated theorem proving
zbMATH Keywords: first-order logic
zbMATH Keywords: binary resolution
zbMATH Keywords: standard contradiction separation
zbMATH Keywords: S-CS dynamic deduction
zbMATH Keywords: ATP systems
MaRDI profile type: Publication
OpenAlex ID: W3137794529
cites work: First-order automated reasoning with theories: when deduction modulo theory meets practice
cites work: System Description: E 1.8
cites work: The 9th IJCAR Automated Theorem Proving System Competition – CASC-J9
cites work: The CADE-27 Automated theorem proving System Competition – CASC-27
cites work: A Machine-Oriented Logic Based on the Resolution Principle
cites work: Handbook of automated reasoning. In 2 vols
cites work: Q3618853
cites work: History and Prospects for First-Order Automated Deduction
cites work: Q5541351
cites work: Automatic Theorem Proving With Renamable and Semantic Resolution
cites work: Stratified resolution
cites work: Geometric Resolution: A Proof Procedure Based on Finite Model Search
cites work: Automated Reasoning
cites work: Simple and Efficient Clause Subsumption with Feature Vector Indexing
cites work: Selecting the Selection
cites work: Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving
cites work: Contradiction separation based dynamic multi-clause synergized automated deduction
cites work: Q5600875
cites work: System Description: Spass Version 3.0
cites work: AVATAR: The Architecture for First-Order Theorem Provers
cites work: Scavenger 0.1: a theorem prover based on conflict resolution
cites work: Limited resource strategy in resolution theorem proving
cites work: Q4797437
cites work: E-MaLeS 1.1
cites work: FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover
cites work: Fingerprint Indexing for Paramodulation and Rewriting
cites work: System Description: E.T. 0.1
cites work: Cooperating Proof Attempts
cites work: Q4672985
DOI: 10.1016/J.INS.2021.03.015
description: scientific article; zbMATH DE number 7763325