On structures of regular standard contradictions in propositional logic

DOI10.1016/J.INS.2021.11.053MaRDI QIDQ6154459zbMATH OpenOpenAlexFDO

Authors Xingxing He, Yingfang Li, Yanghe Feng

Publication date 15 February 2024

Published in Information Sciences (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.ins.2021.11.053

zbMATH Keywords

automated reasoningcontradiction structuresdeductive inference rulespropositional logicregular standard contradictions

Mathematics Subject Classification ID

Computer science (68-XX) Quantum theory (81-XX)

Recommendations

• A multi-clause dynamic deduction algorithm based on standard contradiction separation rule
• Contradiction separation based dynamic multi-clause synergized automated deduction
• Near optimal seperation of tree-like and general resolution
• Proving contradictions in formal theories. I
• Publication:4503913

Cites work

• \(\mathrm{K}_{\mathrm S}\mathrm{P}\) a resolution-based theorem prover for \({\mathsf{K}}_n\): architecture, refinements, strategies and experiments
• A Machine-Oriented Logic Based on the Resolution Principle
• A multi-clause dynamic deduction algorithm based on standard contradiction separation rule
• A superposition calculus for abductive reasoning
• Automatic Theorem Proving With Renamable and Semantic Resolution
• Contradiction separation based dynamic multi-clause synergized automated deduction
• Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
• Extraction of expansion trees
• Formalization of the resolution calculus for first-order logic
• GKC: a reasoning system for large knowledge bases
• Handbook of automated reasoning. In 2 vols
• History and prospects for first-order automated deduction
• scientific article; zbMATH DE number 3254919 (Why is no real title available?)
• scientific article; zbMATH DE number 3320385 (Why is no real title available?)
• scientific article; zbMATH DE number 3415409 (Why is no real title available?)
• iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
• Long-distance Q-resolution with dependency schemes
• On Matrices with Connections
• Restricting backtracking in connection calculi
• System description: E 1.8
• The 9th IJCAR automated theorem proving system competition -- CASC-J9

Cited in

(2)

• A multi-clause dynamic deduction algorithm based on standard contradiction separation rule
• On structures of sign-boundary and diagonal vacancy-type standard contradictions

This page was built for publication: On structures of regular standard contradictions in propositional logic

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