Fully reusing clause deduction algorithm based on standard contradiction separation rule

DOI10.1016/J.INS.2022.11.128MaRDI QIDQ6492544zbMATH OpenFDO

Authors Peiyao Liu, Yang Xu, Jun Liu, Shuwei Chen, Feng Cao, Guanfeng Wu

Publication date 25 April 2024

Published in Information Sciences (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/J.INS.2022.11.128

zbMATH Keywords

ATP systemdeduction algorithminference ruleS-CS rulestandard contradictiontheorem provingvampire

Mathematics Subject Classification ID

Computer science (68-XX) Operations research, mathematical programming (90-XX)

Cites work

• A Machine-Oriented Logic Based on the Resolution Principle
• A multi-clause dynamic deduction algorithm based on standard contradiction separation rule
• A unifying principle for clause elimination in first-order logic
• Automated Reasoning
• Automatic Deduction in an AI Geometry Book
• Automatic Theorem Proving With Renamable and Semantic Resolution
• Contradiction separation based dynamic multi-clause synergized automated deduction
• ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description)
• Faster, higher, stronger: E 2.3
• GKC: a reasoning system for large knowledge bases
• Heterogeneous heuristic optimisation and scheduling for first-order theorem proving
• 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 1737186 (Why is no real title available?)
• Induction in saturation-based proof search
• iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
• Layered clause selection for theory reasoning (short paper)
• Linear resolution with selection function
• Making theory reasoning simpler
• Names are not just sound and smoke: word embeddings for axiom selection
• nanoCoP: a non-clausal connection prover
• Old or heavy? Decaying gracefully with age/weight shapes
• Overview on mechanized theorem proving
• Performance of clause selection heuristics for saturation-based theorem proving
• Proof and model generation with disconnection tableaux
• Restricting backtracking in connection calculi
• SATCHMORE: SATCHMO with RElevancy
• The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
• The TPTP World -- infrastructure for automated reasoning
• Theorem-Proving on the Computer

This page was built for publication: Fully reusing clause 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 Q6492544)