Natural deduction in a paracomplete setting
##plugins.themes.bootstrap3.article.sidebar##
Published:
08.05.2014
##plugins.themes.bootstrap3.article.main##
Abstract
In this paper we present the automated proof search technique in natural deduction paracomplete logic. Here, for some statements we do not have evidence to conclude if they are true or false, as it happens in the classical framework. As a consequence, for example, formulae of the type p _ ¬p, are not valid. In this paper we formulate the natural deduction system for paracomplete logic PComp, explain its main concepts, define proof searching techniques and the searching algorithm providing examples proofs.
##plugins.generic.usageStats.downloads##
##plugins.generic.usageStats.noStats##
##plugins.themes.bootstrap3.article.details##
How to Cite
Bolotov A. E., Shangin V. O. Natural deduction in a paracomplete setting // Logicheskie Issledovaniya / Logical Investigations. 2014. VOL. 20. C. 222-245.
Issue
Section
Papers
References
Avron A. Natural 3-valued logics — characterization and proof theory // The Journal of Symbolic Logic. 1991. Vol. 56(1). P. 276 – 294.
Avron A., Lev I. A formula-preferential base for paraconsistent and plausible non-monotonic reasoning. // Proceedings of the Workshop on Inconsistency in Data and Knowledge (KRR-4), Int. Joint Conf. on AI (Ijcai 2001). 2001. P. 60–70.
Basin D., Matthews S., Vigan`o L. Natural deduction for non-classical logics // Studia Logica. 1998. N. 60(1). P. 119–160.
Batens D. Paraconsistent extensional propositional logics // Logique et Analyse. 1980. Vol. 23. P. 127–139.
Bolotov A. Handling Periodic Properties: Deductive Verification for Quantified Temporal Logic Specifications // Fifth International Conference on Secure Software Integration and Reliability Improvement, SSIRI 2011, 27–29 June, 2011, Jeju Island, Korea. 2011. P. 179–186.
Bolotov A., Basso A., Grigoriev O. Deontic Extension of Deductive Verification of Component Model: Combining Computation Tree Logic and Deontic Logic in Natural Deduction Style Calculus // Proceedings of IICAI-2009. 2009. P. 166–185.
Bolotov A., Shangin. V. Natural Deduction System in Paraconsistent Setting: proof search for PCont // Journal of Intelligent Systems. 2012. Vol. 21. N. 1. P 1–24.
Bolotov A., Basukoski A., Grigoriev O., Shangin V. Natural deduction calculus for linear-time temporal logic. // Joint European Conference on Artificial Intelligence (JELIA-2006). 2006. P. 56–68.
Bolotov A., Grigoriev O., Shangin V. Automated natural deduction for propositional linear-time temporal logic // the Proceedings of the Time-2007, International Symposium on Temporal Representation and Reasoning, June, 2007.
Bolotov A., Bocharov V., Gorchakov A., Makarov V., Shangin V. Let Computer Prove It // Logic and Computer. M.: Nauka, 2004, (In Russian).
Bolotov A., Bocharov V., Gorchakov A., Shangin V. Automated first order natural deduction // Proceedings of the 4th Indian International Conference on Artificial Intelligence (IICAI-2009): Tumkur, 16–18 December 2009. P. 1292–1311.
Bolotov A., Grigoriev O., Shangin V. Natural deduction calculus for computation tree logic // IEEE John Vincent Atanasoff Symposium on Modern Computing. 2006. P. 175–183.
Clarke E., Jha S., Marrero W. R. Using state space exploration and a natural deduction style message derivation engine to verify security protocols // Proceedings of the IFIP TC2/WG 2.2, 2.3 International Conference on Programming Concepts and Methods, June 1998. P. 87–96.
Fitch F. Symbolic Logic. NY: Roland Press, 1952.
Hintikka J. Notes on the quantification theory // Commentationes physico-mathematicae. Societas scientiarum Fennica, 1955. Vol. 12, N. 17.
Jaskowski S. On the rules of suppositions in formal logic // Polish Logic 1920–1939. Oxford Univ. Press, 1967. P. 232–258.
Kamide N. Natural deduction systems for Nelson’s paraconsistent logic and its neighbors // Journal of Applied Non-Classical Logics. 2005. Vol. 15 (4).
Makarov V. Automatic theorem-proving in intuitionistic propositional logic // Modern Logic: Theory, History and Applications. Proceedings of the 5th Russian Conference. StPetersburg, 1998. (In Russian).
Middelburg C. A Survey of Paraconsistent Logics // The Computing Research Repository (CoRR). Vol.1103.4324, 2011.
Naddeo A. Axiomatic Framework applied to Industrial Design Problem formulated by Para-complete logics approach: the power of decoupling on Optimization-Problem solving // Proceedings of Fourth International Conference on Axiomatic Design. 2006. P 1–8.
Nelson D. Constructible falsity // Journal of Symbolic Logic. 1949. Vol. 14. P. 16–26.
Pfenning F. Logical frameworks // Handbook of Automated Reasoning, J. A. Robinson and A. Voronkov eds. Elsevier, 2001. Chapter XXI, P. 1063–1147.
Popov V. Sequence axiomatisation of simple paralogics // Logical Investigations. 2010. Issue 16. P. 205–220. (In Russian).
Quine W. On natural deduction // Journal of Symbolic Logic. 1950. Vol. 15. P. 93–102.
Shangin V. Natural deduction systems of some logics with truth-value gluts and truth-value gaps // Logical investigations. M.-SPb: C.G.I., 2011. P. 293–308. (in Russian).
Sieg W., Byrnes J. Normal natural deduction proofs (in classical logic) // Studia Logica. 1998. Vol. 60. P. 67–106.
Wooldridge M. Reasoning about Rational Agents. MIT Press, 2000.
Avron A., Lev I. A formula-preferential base for paraconsistent and plausible non-monotonic reasoning. // Proceedings of the Workshop on Inconsistency in Data and Knowledge (KRR-4), Int. Joint Conf. on AI (Ijcai 2001). 2001. P. 60–70.
Basin D., Matthews S., Vigan`o L. Natural deduction for non-classical logics // Studia Logica. 1998. N. 60(1). P. 119–160.
Batens D. Paraconsistent extensional propositional logics // Logique et Analyse. 1980. Vol. 23. P. 127–139.
Bolotov A. Handling Periodic Properties: Deductive Verification for Quantified Temporal Logic Specifications // Fifth International Conference on Secure Software Integration and Reliability Improvement, SSIRI 2011, 27–29 June, 2011, Jeju Island, Korea. 2011. P. 179–186.
Bolotov A., Basso A., Grigoriev O. Deontic Extension of Deductive Verification of Component Model: Combining Computation Tree Logic and Deontic Logic in Natural Deduction Style Calculus // Proceedings of IICAI-2009. 2009. P. 166–185.
Bolotov A., Shangin. V. Natural Deduction System in Paraconsistent Setting: proof search for PCont // Journal of Intelligent Systems. 2012. Vol. 21. N. 1. P 1–24.
Bolotov A., Basukoski A., Grigoriev O., Shangin V. Natural deduction calculus for linear-time temporal logic. // Joint European Conference on Artificial Intelligence (JELIA-2006). 2006. P. 56–68.
Bolotov A., Grigoriev O., Shangin V. Automated natural deduction for propositional linear-time temporal logic // the Proceedings of the Time-2007, International Symposium on Temporal Representation and Reasoning, June, 2007.
Bolotov A., Bocharov V., Gorchakov A., Makarov V., Shangin V. Let Computer Prove It // Logic and Computer. M.: Nauka, 2004, (In Russian).
Bolotov A., Bocharov V., Gorchakov A., Shangin V. Automated first order natural deduction // Proceedings of the 4th Indian International Conference on Artificial Intelligence (IICAI-2009): Tumkur, 16–18 December 2009. P. 1292–1311.
Bolotov A., Grigoriev O., Shangin V. Natural deduction calculus for computation tree logic // IEEE John Vincent Atanasoff Symposium on Modern Computing. 2006. P. 175–183.
Clarke E., Jha S., Marrero W. R. Using state space exploration and a natural deduction style message derivation engine to verify security protocols // Proceedings of the IFIP TC2/WG 2.2, 2.3 International Conference on Programming Concepts and Methods, June 1998. P. 87–96.
Fitch F. Symbolic Logic. NY: Roland Press, 1952.
Hintikka J. Notes on the quantification theory // Commentationes physico-mathematicae. Societas scientiarum Fennica, 1955. Vol. 12, N. 17.
Jaskowski S. On the rules of suppositions in formal logic // Polish Logic 1920–1939. Oxford Univ. Press, 1967. P. 232–258.
Kamide N. Natural deduction systems for Nelson’s paraconsistent logic and its neighbors // Journal of Applied Non-Classical Logics. 2005. Vol. 15 (4).
Makarov V. Automatic theorem-proving in intuitionistic propositional logic // Modern Logic: Theory, History and Applications. Proceedings of the 5th Russian Conference. StPetersburg, 1998. (In Russian).
Middelburg C. A Survey of Paraconsistent Logics // The Computing Research Repository (CoRR). Vol.1103.4324, 2011.
Naddeo A. Axiomatic Framework applied to Industrial Design Problem formulated by Para-complete logics approach: the power of decoupling on Optimization-Problem solving // Proceedings of Fourth International Conference on Axiomatic Design. 2006. P 1–8.
Nelson D. Constructible falsity // Journal of Symbolic Logic. 1949. Vol. 14. P. 16–26.
Pfenning F. Logical frameworks // Handbook of Automated Reasoning, J. A. Robinson and A. Voronkov eds. Elsevier, 2001. Chapter XXI, P. 1063–1147.
Popov V. Sequence axiomatisation of simple paralogics // Logical Investigations. 2010. Issue 16. P. 205–220. (In Russian).
Quine W. On natural deduction // Journal of Symbolic Logic. 1950. Vol. 15. P. 93–102.
Shangin V. Natural deduction systems of some logics with truth-value gluts and truth-value gaps // Logical investigations. M.-SPb: C.G.I., 2011. P. 293–308. (in Russian).
Sieg W., Byrnes J. Normal natural deduction proofs (in classical logic) // Studia Logica. 1998. Vol. 60. P. 67–106.
Wooldridge M. Reasoning about Rational Agents. MIT Press, 2000.