Natural Deduction Theorem Proving Techniques in Classical and non-Classical Logics: About the Project


 

 

MEMBERS:

 

University of Westminster:

 

Alexander Bolotov     

Artie Basukoski

Gaurav Gupta

 

Moscow State University

Oleg Grigorev

Vasili Shangin

Dmitri Zaitzev

 

This long term research project was initially set up within the Faculty of Philosophy, Moscow State University (1995-1998) by Alexander Bolotov, Vyacheslav Bocharov and Alexander Gorchakov, when we developed and implemented natural deduction (ND) technique for the classical propositional logic (CPL). Initially we were interested in the development of the proof search procedure for a Fitch style ND system for CPL. You can try a Windows based implementation which you can obtain from us by correspondence. The search procedure appeared to be generic enough to be extended into First-Order Logic by Vasilyi Shangin, and to Intuitionistic Logic by V.Makarov. Later, Oleg Grigoriev, Artie Basukoski and Gaurav Gupta joined the group and we have defined natural deduction calculi for propositional Linear-time Temporal Logic (PLTL) and Computation Tree Logic (CTL) and the deontic extension of the latter logic. We have recently worked on the development of the natural deduction system for the Propositional Linear-time Temporal Logic extended with Propositional Quantification (QPTL), please see our technical report on these latest developments.

 

Main Results

 

  • Full automation of the Fitch-style natural deduction in Classical Propositional Logic and its implementation as an automatic theorem-prover;
  • Extension of the proof searching algorithm to the First-order setting, Temporal and Paraconsistent Logics.

 

Main Publications


 

Books

[1] Let Computer Prove It. Series: Logic and Computer. Authors: V. Bocharov, A. Bolotov, A. Gorchakov, V. Makarov and V.Shangin. Moscow, Nauka 2004 (in Russian).

Journal Articles

 

[2]  A. Bolotov and V. Shangin. Natural Deduction System in Paraconsistent Setting: Proof Search for PCont. Journal of Intelligent Systems, Volume 21, Issue 1, Pages 1–24, ISSN (Online) 2191-026X, ISSN (Print) 

     0334-1860,DOI: 10.1515/jisys-2011-0021, February 2012

 

[3] V. Shangin. Natural Deduction Systems for logics with truth-value gluts and truth-value gaps. Logical Investigations, editor A. Karpenko, Institute of Philosophy, Russian Academy of Sciences, ISBN 978-5-98712-073-6. pages. 293-308.

(In Russian.) Системы натурального вывода для некоторых логик с истинностными провалами и логик с пресыщенными оценками // Логические исследования / Отв. ред. А.С. Карпенко; Ин-т философии РАН; философский ф-т МГУ им. М.В. Ломоносова. М.-СПб.: ЦГИ, 2011. Вып. 17 – ISBN 978-5-98712-073-6. С. 293-308.

 

[4]  A. Bolotov, A. Basukoski, O. Grigoryev, and V. Shangin.Natural deduction system for linear time temporal  logic. Logical Investigations, Volume 13, (in Russian), pages 17-95, Nauka, Moscow (2007). ISBN 5-

     02-035152-0.

 

[5] Shangin V. Automated natural deduction in intuitionistic logic and the duplication problem // Aspects, Vol. 2, M., Sovremennye tetradi, 2003 (in Russian).

 

[6] Shangin V. Correctness theorem for an algorithm for searching for natural deduction in classical propositional logic // On-line journal "Logical Studies", Vol. 4, 2000 (in Russian), available at http://www.logic.ru/Russian/LogStud/04/No4-02.html.

 

[7] A. Bolotov, A V. Bocharov and A. Gorchakov, and  Proof Searching Algorithm in Classical Predicate Calculus (with). Logical Investigations, Volume 5, 1998 (in Russian), Nauka, Moscow. ISBN 5-02-01-3682-4.

 

Conference/workshop  Proceedings

 

[8] A. Bolotov and V. Shangin. Natural Deduction in the setting of Paraconsistent Logic. Proceedings of the 19th Automated Reasoning  Workshop 2012 (ARW2012), Renate A. Schmidt; Fabio Papacchini, editors, Pages 15-16, Technical Report, Department of Computing Science, University of Manchester, Glasgow, April

04th – 05th,, available from Manchester eScholar https://www.escholar.manchester.ac.uk/uk-ac-man-scw:161817

 

[9] Popov V., Shangin V. In the vicinity of Sette logic // Proceedings of the 14th International Congress of Logic Methodology and Philosophy of Science. Nancy University, Nancy, France, July 19-26, 2011.

 

[10] A. Bolotov. Handling Periodic Properties: Deductive Verification for Quantified Temporal Logic Specifications. Proceedings of the 5th IEEE International Conference on Secure Software Integration & Reliability 

      Improvement Companion (SSIRI-C), pages: 179 – 186, Jeju Island, 27-29 June 2011, Print ISBN: 978-14577-0781-0.

 

[11]  A. Bolotov and V. Shangin. And Natural deduction system in paraconsistent setting: proof search for PCont. In the Proceedings of the 5th Indian International Conference on Artificial Intelligence (IICAI-2011), Tumkur, (2011), 630–638.

 

[12] A. Bolotov and V. Shangin. Natural Deduction in the setting of Paraconsistent Logic. Proceedings of the 18th Automated Reasoning  Workshop 2011 (ARW2011), Pages 28-19, Technical Report, Department of Computing Science, University of Glasgow, Glasgow, April 11th – 12th.

 

[13] Shangin V. Natural Deduction Systems for Logics  Par, PCont, and PComp. (In Russian). Russian Conference on Logic Methodology and Scientology”, Octover 2010. Системы натурального вывода для логик Par, PCont, PComp и PContPComp // Всероссийская научная конференция «Логика, методология, науковедение: актуальные проблемы и перспективы»,  Ростов-на-Дону, 4-6 октября 2010

 

[14] Shangin V. Natural Deduction Systems for Paraconsistent Logics induced by Arruda’s logic VI. (in Russian) Системы натурального вывода для паранепротиворечивых логик, родственных логике, индуцированной исчислением V1 А. Арруда // Международная конференция «Воображаемая логика» Н.А. Васильева и современные неклассические логики», 11-15 октября, Казань, 2010, pp. 106-108.

 

[15] A. Bolotov, A. Basso and O.Grigoriev Deontic Extension of Deductive Verification of Component Model: Combining Computation Tree Logic and Deontic Logic in Natural Deduction Style Calculus. In Proceedings of the 4th Indian International Conference on Artificial Intelligence (IICAI-09), December 16-18, 2009, Tumkur, India.

 

[16] A. Bolotov.  On the "Until induction" in natural deduction for PLTL. International conference  "6th Smirnov's Readings in Logic" June 17 - 19, 2009, Moscow (Russia).

 

[17] Bolotov, Alexander and Grigoriev, Oleg and Shangin, Vasilyi (2008) Automating natural deduction for temporal logic. In:Glymour, Clark and Wang, Wei and Westerstahl, Dag, (eds.) Proceedings of the 13th International Congress of Logic Methodology and Philosophy of Science.

 

[18] A. Bolotov and O.Grigoriev Natural Deduction Calculus for Quantified Propositional Linear-time Temporal Logic (QPTL) (QPTL). The 16th Workshop on Automated Reasoning, (ARW 2008), University of Liverpool, April 2009.

 

[19] A. Bolotov. Tackling ”Until Induction” in Natural Deduction for PLTL. The 15th Workshop on Automated Reasoning, (ARW 2008), University of Birmingham, July 2008.

[20] A. Bolotov, O. Grigoriev and V. Shangin.A Simpler Formulation of Natural Deduction Calculus for Linear-Time Temporal Logic. In Proceedings of the 3d Indian International Conference on Artificial Intelligence (IICAI-07), Puna, India, Pages 1253-1266.

[21] A. Bolotov, O. Grigoriev and V. Shangin. Automated Natural Deduction for Propositional Linear-time Temporal Logic . In Proceedings of the 13th International Congress of Logic Methodology and Philosophy of Science. Tsinghua University , Beijing , China , August 9-15, 2007.

[22] A. Bolotov, O. Grigoriev and V. Shangin. Automating natural deduction for linear-time temporal logic. In Proceedings of the 14th International Symposium on Temporal Representation and Reasoning, 2007. TIME 2007, pages 47-58, 2007.

 

[23] A. Bolotov, O. Grigoriev and V. Shangin. Buy one get two free: a simpler formulation of natural deduction for computation tree logic CTL (with O.Grigoriev and V.Shangin). Proceedings of the “Smirnov’s Readings”, VI International Conference, Moscow State University, June 2007.

 

[24] A. Bolotov, O. Grigoriev and V. Shangin Automating Natural Deduction for Temporal Logic. The 14th Workshop on Automated Reasoning, (ARW 2007), Imperial College, April 2007.

 

[25] A. Bolotov, A. Basukoski ,O. Grigoriev and V. Shangin Natural Deduction Calculus For Linear-Time Temporal Logic. In Logics in Artificial Intelligence, Proceedings of 10th European Conference (JELIA 2006), Volume 4160 of Lecture Notes in Computer Science, Liverpool, September 2006, pages 56-68.

[26] A.Bolotov, V. Bocharov and A. Gorchakov  Proof Searching Algorithm in Classical Propositional Natural Deduction Calculus. Logical Investigations, Proceedings of the Research Logical Seminar of the Institute of Philosophy, Russian Academy of Sciences,  (in Russian), pages 181-186, Russian Academy of Sciences, Moscow, 1996. ISBN 5-201-01952-8.

 

[27] A. Bolotov, O. Grigoriev and V. Shangin. Natural Deduction Calculus For Computation Tree Logic (with O. Grigoryev and V. Shangin). Proceedings of IEEE 2006 John Vincent Atanasoff International Symposium on Modern Computing, 3-6 October 2006, Sofia, Bulgaria, pages 175-183.

 [28] A.Bolotov, V. Bocharov and A. Gorchakov and V. Shangin.  Automatic First Order Natural Deduction. Proceedings of the 2nd Indian International Conference on Artificial Intelligence (IICAI-05), Puna, India, 2005, pages 1292-1311.

[29] Shangin V. A new proof of soundness theorem for natural deduction in classical predicate calculus In Proceedings of the International conference "Logic: history, theory and its application", St.-Petersburg (2004). St.-Petersburg, 2004. (in Russian)

 

 [30] V.Shangin. Doctor of Philosophy (equiv.), obtained from the Moscow State University. Thesis title: Automated Natural Deduction for Classical First-order logic (in Russian) under supervision of Prof. V. Bocharov and Dr. A. Bolotov.

 

[31] Proof-searching Algorithm in First Order Classical Natural Deduction Calculus (with A. Bocharov, A. Gorchakov and V. Shangin.). In Proceedings of 12th International Congress on Logic Philosophy and Methodology of Science, Oviedo, August 2003. 

 

[32] Shangin V. Some metatheoretical properties of natural deduction // Proceedings of the International conference “Smirnov’s readings”, Moscow (2003). Moscow, 2003. (in Russian)

 

[33] Shangin V. Automated natural deduction in intuitionistic logic and the duplication problem In Proceedings of the International conference "Logic: history, theory and its application", St.-Petersburg (2002). St.-Petersburg, 2002. (in Russian)

 

[34] Shangin V. Correctness theorem for an algorithm for searching for natural deduction in classical propositional logic In Proceedings of the International conference "Logic: history, theory and its application", St.-Petersburg (2000), pages 175-176, St. Petersburg, 2000. (in Russian)

 

[35]  V. Makarov. Automatic theorem-proving in intuitionistic propositional logic. In Modern Logic: Theory, History and Applications. Proceedings of the 5th Russian Conference, StPetersburg, (in Russian), 1998.

 

[36] A. Bolotov. Automating Natural Deduction. Proceedings of the 11th International Congress of Logic, Methodology and Philosophy of Science (Crakow, Poland, August 1999)

 

[37] A.Bolotov Bocharov and A. Gorchakov.  Natural Deduction Proof Searching Algorithm for the Classical Propositional Calculus. VProceedings of the XI International Conference on Logic, Methodology and Philosophy of Science, part 2, Obninsk, 1995 (in Russian).

 

[38] A. Bolotov. Informational and Algebraic Approaches to the Analysis of the Logical Entailment in Classical andRelevant Logic. PhD, Moscow State University, 1992 (in Russian).

Technical Reports

[39] A. Bolotov and O. Grigoriev. Natural Deduction System for the Deontic Extension of Computation Tree Logic (CTL), Technical Report, Distributed and Intelligent Systems Group, University of Westminster, 2009.

[40] A. Bolotov and O. Grigoriev. Natural Deduction for propositional linear-time temporal logic (PLTL) extended with propositional quantification. Technical Report, Distributed and Intelligent Systems Group, University of Westminster, 2009.