On structures of regular standard contradictions in propositional logic

DOI10.1016/J.INS.2021.11.053OpenAlexW3216154863MaRDI QIDQ6154459FDOQ6154459

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

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

zbMATH Keywords

automated reasoningpropositional logiccontradiction structuresdeductive inference rulesregular standard contradictions

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (1)

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

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)