Alexander Bolotov's Publications

Some of the publications below are available electronically. Otherwise, please contact me if you require a copy. You can also download my Research Profile.



 

Edited Volumes

Proceedings of the Automated Reasoning Workshop 2010: Bridging the Gap between Theory and Practice, ARW 2010. University of Westminster, London.

 

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]   Natural Deduction System in Paraconsistent Setting: Proof Search for PCont (with V. Shangin). 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]  Natural deduction system for linear time temporal  logic (with A. Basukoski, O. Grigoryev, and  V. Shangin) Logical Investigations, Volume 13, (in Russian), pages 17-95, Nauka, Moscow (2007). ISBN 5-

     02-035152-0.

 

[4] A Clausal Resolution Method for Branching Time Logic ECTL+ (with A. Basukoski). Annals of Mathematics and Artificial Intelligence, Springer, 46(3): 235-263

    (2006), ISSN: 1012-2443 (Print) 1573-7470 (Online), http://dx.doi.org/10.1007/s10472-006-9018-1. Available on-line from Springer.

[5] Clausal Resolution for Extended Computation Tree Logic ECTL (with A. Basukoski). Journal of Applied Logic, Elsevier, 4(2): 141-167 (2006), http://dx.doi.org/10.1016/j.apal.2005.03.002.

[6] Alternating Automata and Temporal Logic Normal Forms (with C. Dixon and M. Fisher). Annals of Pure and Applied Logic, Volume 135, Issues 1-3, September 2005, Pages 263-285, Elsevier. http://dx.doi.org/10.1016/j.apal.2005.03.002. Available online from Sciencedirect.

[7] The Scientist and His Time (with D. Zaitzev). Logical Studies, vol. 10, 2003. Special Issue on the works of Distinguished Professor of Moscow State University E.Voishvillo (in Russian). ISBN 5-02-006257-X

 

[8] On the Relationship between Normal Form and “w”-automata (with M. Fisher and C. Dixon). Journal of Logic and Computation, Volume 12, Issue 4, August 2002, pages 561-581, Oxford University Press, ISSN: 0955-792X. http://www3.oup.co.uk/logcom/hdb/Volume_12/Issue_04/120561.sgm.abs.html.

 

[9] Resolution in a Logic of Rational Agency (with C. Dixon and M. Fisher). Artificial Intelligence, volume 139, issue 1, July 2002, pages 47-89, Elsevier Science, http://dx.doi.org/10.1016/S0004-3702(02)00196-0. Available online from Sciencedirect.

[10] A Clausal Resolution Method for CTL Branching Time Temporal Logic (with M. Fisher). Journal of Experimental and Theoretical Artificial Intelligence, volume 11, 1999, pages 77-93, Taylor & Francis. ISSN: 1362-3079 (electronic) 0952-813X (paper). Draft version.

 

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

 

 

Conference/workshop  Proceedings

 

[12]  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.

 

[13]  Natural deduction system in paraconsistent setting: proof search for PCont (with V. Shangin). In the Proceedings of the 5th Indian International Conference on Artificial Intelligence (IICAI-2011), Tumkur

       (2011), 630–638.

 

[14] Natural Deduction in the setting of Paraconsistent Logic (with V.Shangin). 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.

 

[15] Invariant-Free Deduction for CTL*: The Tableau Method (with Jose Gaintzarain and Paqui Lucio) The 17th Workshop on Automated Reasoning, (ARW 2010), University of Westminster, March 2010.

 

[16] Towards symbolic reasoning from subsymbolic sensory information (with Gaurav Gupta and Aleka Psarrou) The 17th Workshop on Automated Reasoning, (ARW 2010), University of Westminster, March 2010.

 

[17] Safety and Liveness of Component-oriented Protocols: A Feasibility Study (with Shamima Paurobally and Vladimir Getov) The 17th Workshop on Automated Reasoning, (ARW 2010), University of Westminster, March 2010.

 

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

 

[19] Temporal Specification and Deductive Verification of a Distributed Component Model and Its Environment. (with A. Basso, and V. Getov). Proceedings of the workshop Model-Based Verification and Validation in conjunction with the 3rd IEEE International Conference on Secure Software Integration and Reliability Improvement (SSIRI)', Shanghai, China, July 2009.

 

[20]  Multi-Agent Systems in engineering of e-commerce and e-business systems (with S. Maltseva), RIW 2009: Russian Internet Week, Joint exhibition presentations (http://www.rocid.ru/person/41190/).

 

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

 

[22] State-Based Behavior Specification for GCM Systems (with A. Basso, and V. Getov). The 16th Workshop on Automated Reasoning, (ARW 2008), University of Liverpool, April 2009.

 

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

 

[24] Behavioural model of component-Based Grid Environments (with A. Basso and V.Getov)  In T. Priol and M. Vanneschi (Ed.), From Grids to Service and Pervasive Computing. Proceedings of the CoreGrid Symposium 2008, Las Palmas, Canary Island, August 2008 in conjunction with EUROPAR, Springer, 2008, pages 19-30, ISBN 978-0-387-78447-2.

 

[25] Tackling ”Until Induction” in Natural Deduction for PLTL. The 15th Workshop on Automated

       Reasoning, (ARW 2008), University of Birmingham, July 2008.

 

[26] Automata-based Formal Specification of Stateful Systems (with Alessandro Basso and Vladimir Getov)  The 15th Workshop on Automated Reasoning, (ARW 2008), University of Birmingham, July 2008.

 

[27] Towards GCM re-configuration - extending specification by norms (with A. Basso) In Marco Danelutto, Paraskevi Fragopoulou and Vladimir Getov (Editors) Making Grids Work. Proceedings of the CoreGRID Workshop on Programming Models Grid and P2P System Architecture Grid Systems, Tools and Environments, 12-13 June 2007, Heraklion, Crete, Greece, Springer, 2007, pages 17-29, ISBN 978-0-387-09454-0.

 

 

[28] A Simpler Formulation of Natural Deduction Calculus for Linear-Time Temporal Logic (with O.

Grigoriev and V. Shangin.). In Proceedings of the 3d Indian International Conference on Artificial Intelligence (IICAI-07), Puna, India, Pages 1253-1266.

[29] Automated Natural Deduction for Propositional Linear-time Temporal Logic (with Oleg Grigoriev and Vasilyi Shangin:) In Proceedings of the 13th International Congress of Logic Methodology and Philosophy of Science. Tsinghua University , Beijing , China , August 9-15, 2007.

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

 

[31] 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.

 

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

 

[33] Verification tool Grid component system (with A.Basso). The 14th Workshop on Automated Reasoning, (ARW 2007), Imperial College, April 2007.

[34] Natural Deduction Calculus For Linear-Time Temporal Logic (with A. Basukoski, O. Grigoryev, and V. Shangin). 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.

[35]   Proof Searching Algorithm in Classical Propositional Natural Deduction Calculus (with V. Bocharov and A. Gorchakov). 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.

[36] Clausal Resolution for ECTL+: Complexity Analysis (with A. Basukoski). Proceedings of IEEE 2006 John Vincent Atanasoff International Symposium o Modern Computing, 3-6 October 2006, Sofia, Bulgaria, pages 1-6 (Young Researchers Session).

[37] Specifcation and Verifcation of Reconfguration Protocols in Grid Component Systems (with Alessandro Basso, Artie Basukoski, Vladimir Getov, Ludovic Henrio, and Mariusz Urbanski) In the Proceedings of the 3d IEEE Conference on Intelligent Systems (IS-2006), September 2006.

 

[38] Search and Check. Problem Solving by Problem Reduction (with P. Lupkowski and M. Urbanski). In the Proceedings of The 8th International Conference on Artificial Intelligence and Soft Computing, Zakopane, Poland, June 2006. (Polish Neural Networks Society and the Academy of Humanities and Economics (Lodz) in cooperation with the Department of Computer Engineering at Czestochowa University of Technology and the IEEE Computational Intelligence Society).

 

[39] 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.

[40] Specifcation and Verifcation of Reconfguration Protocols in Grid Component Systems (with A. Basso, A. Basukoski, V. Getov, L. Henrio, and M. Urbanski). The 13th Workshop on Automated Reasoning, (ARW 2006), Bristol, July 2006.

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

[42] Search Strategies for Resolution in CTL-Type Logics: Extension and Complexity, (with A. Basukoski). Proceedings of the 12th International Symposium on Temporal Representation and Reasoning, 2005. TIME 2005. 23-25 June 2005,  IEEE Computer Society 2005, pages 195 - 197.

[43] Clausal Resolution in the Framework of Social Agency (with I. Swigkos) The 12th Workshop on Automated Reasoning, (ARW 2005), Edinburgh, 2005.

[44] Clausal Resolution for Extended Computation Tree Logic ECTL+ (with A. Basukoski). Proceedings of the Time 2004 International Conference on Temporal Representation and Reasoning, France, Tatihou, July 2004, pages 140-147.

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

[46] Clausal Resolution for Extended Computation Tree Logic ECTL. Proceedings of the Time-2003/ICTL-2003 International Conference on Temporal Representation and Reasoning/International Conference on Temporal Logic (Australia, July 2003), IEEE Computer Society, 2003, pages 107-117.

 

[47] Resolution for Branching Time Temporal Logics.  Smirnov's Readings. 4th International Conference, Moscow, 2003.

 

[48] Clausal Resolution for Extended Computation Tree Logic ECTL. 10th Workshop on Automated        

      Reasoning,  AR2003, Liverpool, 2003.

 

[49] Resolution for Branching Time Temporal Logics: Applying the Temporal Resolution Rule (with C. Dixon). Proceedings of the Time-2000 International Conference on Temporal Representation and Reasoning (Nova Scotia, Canada, July 2000), IEEE Computer Society, 2000, pages 163-172.

 

[50] Resolution in a Logic of Rational Agency (with C. Dixon - main contributor, and M. Fisher).  Proceedings of the 14th European Conference on Artificial Intelligence (Berlin, August 2000), IOS Press.

 

[51] On the Relationship between Normal Form and `w’-automata (with M. Fisher and C. Dixon).  Proceedings of the Advances in Modal Logic - International Conference on Temporal Logic 2000 (University of Leipzig, October 2000), pages 13-22.

 

[52] Automata on Infinite Words and Temporal Logic Normal Forms. 7th Workshop on Automated Reasoning (AR2000), King’s College, London, 2000.

 

[53] General Normal Form for Temporal Logic. British Colloquium of Theoretical Computer Science (BCTCS16), Liverpool, 2000.

 

[54] Clausal Resolution for Branching-Time Logic (with M. Fisher). Proceedings of the 11th International Congress of Logic, Methodology and Philosophy of Science (Crakow, Poland, August 1999), pages 137-148.

 

[55] Clausal Resolution for CTL* (with C. Dixon, and M. Fisher) Mathematical Foundations of Computer Science, Proceedings of the 24th International Symposium (MFCS'99), (Poland, August 1999), volume 1672 of Lecture Notes in Computer Science, Springer, 1999, pages 137-148.

 

[56] Clausal Resolution for Branching-Time Temporal Logics and Temporal Mu-Calculus. 6th Workshop on Automated Reasoning, Edinburgh, 1999.

 

[57] A Resolution Method for CTL Branching-Time Temporal Logic (with M. Fisher). Proceedings of the 4th International Workshop on Temporal Representation and Reasoning (TIME'97) (Florida, 1997), IEEE Computer Society, pages 20-27.

 

[58] Clausal Resolution for CTL. British Colloquium of Theoretical Computer Science (BCTCS13), Sheffield, 1997.

 

[59] Can Relevant Logic Solve Aristotle's Problem of Fatalism? (with E. Voishvillo). Proceedings of the 12th International Philosophical Congress, Moscow, 1993 (in Russian).

 

[60] On Meyer's Reduction to 2-nd Degree Formulae and its Methodological Significance in Relevant Logic. Proceedings of the 10th Conference on Logic, Philosophy and Methodology of Science, Moscow, 1990 (in Russian).

 

 

KeyNOTE TALKS, MAIN Invited LECTURES and Talks

 

       K1    Application of Logic for Software Modelling and Deductive Verification. Keynote talk at the International Conference on Information, Communication and Embedded Systems, ICICES-2011,                       

               S.A. Engineering College, Chennai, 23-24 February 2011 (Keynote Talk). 

T1.  Automating of Natural Deduction theorem proving and its applications. Invited Lecture, University of San Sebastian, September 2012.

T2.  Automation of the Natural Deduction Calculus for Temporal Logic. Research Seminars, University of Manchester and University of Liverpool, 2007.

T3.  Clausal Resolution in the Framework of Normative Agency. Dagstuhl Seminar on Normative Multi-Agent Systems, March 18-23, 2007.

T4.  Natural Deduction Calculus For Computation Tree Logic. 2006 John Vincent Atanasoff International Symposium on Modern Computing, 3-6 October 2006, Sofia , Bulgaria.

T5.  Formal Specification and Verification in the Branching-Time Setting. Logical Theory Research Seminar Series, Faculty of Philosophy, Moscow State University, April 2004.

T6.  Formal Verification of Temporal Specifications - a Resolution Based Approach. Research Seminar Series, University of Greenwich, November 2001.

T7.  Clausal Resolution for Linear-Time Temporal Mu-calculus. Workshop on Fixpoint and First-Order Temporal Logics. University of Liverpool, September, 2001.

T8.  Clausal Resolution for Temporal Mu-Calculus. Research Seminar of the Foundation of Computer Science Laboratory, University of Edinburgh, 2000.

T9.  Verification Methods for Temporal Logics. Lomonosov’s Readings, Faculty of Philosophy, Moscow State University, April, 1998.

T10.                      Clausal Resolution for Branching-Time Temporal Logics. 1st Temporal Logic Workshop. Free University, Amsterdam, October 1997.

T11.                      Informational Approach to the Analysis of the Logical Entailment in Classical and Relevant Logic. Theory Seminar, Indiana University, Bloomington, 1994.

 

Other Publications (Technical Reports, Drafts, etc)

 

Natural Deduction System for the Deontic Extension of Computation Tree Logic (CTL). (Technical report)

Natural Deduction for propositional linear-time temporal logic (PLTL) extended with propositional quantification. (Technical report)