A reasoning method for a paraconsistent logic
The recognition of the importance of paraconsistency for the study of the problem of modelling and automatizing the reasoning required to produce a glimmer of intelligent behavior on machines appeared in several previous works of the authors. This paper presents a proof method for automation of reasoning in the known paraconsistent predicate calculus \(C^*_ 1\) of da Costa. The method is analytical, using a specially designed tableau system. The reasoning method presented here is a tableau system sound and complete for \(C^*_ 1\), actually two tableau systems being developed. The system \(SC^*_ 1\) is presented with sketches for the proofs of its soundness and completeness with respect to the semantics of \(C^*_ 1\), being not suitable, meanwhile, for implementation. The system \(S'C^*_ 1\), a conservative extension of \(SC^*_ 1\) designed to enable better implementation, is then described. It has more rules, which prove to produce smaller trees than those resulting from the applications of the rules in \(SC^*_ 1\). The two systems are equivalent in the sense that they are able to prove the same theorems. A prototype based on \(S'C^*_ 1\) was effectively implemented and the authors suggest its improvement as a prover.
- A decidable paraconsistent relevant logic: Gentzen system and Routley-Meyer semantics
- Analytical tableaux for da Costa's hierarchy of paraconsistent logics \(C_n\), \(1\leq n<\omega\)
- Reducing Preferential Paraconsistent Reasoning to Classical Entailment
- A Logic for Ambiguous Description
- Analytical tableaux for da Costa's paraconsistent predicate calculi C_n^*
- Towards an efficient prover for the \(C_1\) paraconsistent logic
- A method of defining paraconsistent tableaus
- A logic for reasoning with inconsistency
- A logical expression of reasoning
This page was built for publication: A reasoning method for a paraconsistent logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q687160)
