
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) 2191026X, ISSN
(Print)
03341860,DOI: 10.1515/jisys20110021,
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 1795, Nauka, Moscow (2007). ISBN 5
020351520.
[4] A Clausal Resolution
Method for Branching Time Logic ECTL+ (with A. Basukoski).
Annals of Mathematics and Artificial Intelligence, Springer, 46(3): 235263
(2006), ISSN: 10122443 (Print) 15737470
(Online), http://dx.doi.org/10.1007/s1047200690181.
Available online from Springer.
[5] Clausal Resolution for Extended
Computation Tree Logic ECTL (with A. Basukoski). Journal of Applied
Logic, Elsevier, 4(2): 141167 (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 13, September 2005,
Pages 263285, 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
502006257X
[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 561581,
Oxford University Press, ISSN:
0955792X. 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
4789, Elsevier Science, http://dx.doi.org/10.1016/S00043702(02)001960.
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 7793, Taylor & Francis. ISSN:
13623079 (electronic) 0952813X (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 5020136824.
Conference/workshop
Proceedings
[12]
Handling Periodic Properties: Deductive Verification for Quantified
Temporal Logic Specifications. Proceedings of the 5^{th}
IEEE International Conference on Secure Software Integration &
Reliability
Improvement Companion (SSIRIC), pages:
179 – 186, Jeju
Island, 2729 June
2011, Print ISBN: 9781457707810.
[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 (IICAI2011), Tumkur
(2011), 630–638.
[14] Natural Deduction in the setting of
Paraconsistent Logic (with V.Shangin). Proceedings of the 18^{th}
Automated Reasoning Workshop 2011
(ARW2011), Pages 2819, Technical Report, Department of
Computing Science, University of Glasgow,
Glasgow, April 11th – 12^{th}.
[15] InvariantFree Deduction for CTL*:
The Tableau Method (with Jose Gaintzarain and Paqui Lucio) The 17^{th}
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 17^{th} Workshop on Automated
Reasoning, (ARW 2010), University of Westminster, March
2010.
[17] Safety and Liveness of Componentoriented Protocols: A
Feasibility Study (with Shamima Paurobally and Vladimir Getov) The 17^{th}
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
(IICAI09), December 1618, 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 ModelBased Verification and Validation in
conjunction with the 3rd IEEE International Conference on Secure Software
Integration and Reliability Improvement (SSIRI)', Shanghai, China,
July 2009.
[20] MultiAgent Systems in engineering of
ecommerce and ebusiness 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] StateBased
Behavior Specification for GCM Systems (with A. Basso, and V.
Getov). The 16^{th} Workshop on Automated
Reasoning, (ARW 2008),
University of Liverpool, April 2009.
[23]
Natural
Deduction Calculus for Quantified Propositional Lineartime Temporal Logic
(QPTL) (QPTL) (with O. Grigoriev). The 16^{th} Workshop
on Automated Reasoning, (ARW
2008), University
of Liverpool, April
2009.
[24] Behavioural model of componentBased
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 1930, ISBN
9780387784472.
[25] Tackling ”Until Induction” in Natural Deduction for PLTL. The 15^{th}
Workshop
on Automated
Reasoning, (ARW 2008), University of Birmingham,
July 2008.
[26] Automatabased Formal Specification of Stateful Systems (with Alessandro Basso and
Vladimir Getov) The 15^{th} Workshop on Automated Reasoning, (ARW 2008), University of Birmingham,
July 2008.
[27] Towards
GCM reconfiguration  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, 1213 June
2007, Heraklion, Crete, Greece, Springer, 2007, pages
1729, ISBN 9780387094540.
[28] A Simpler Formulation of Natural Deduction
Calculus for LinearTime Temporal Logic (with O.
Grigoriev and V. Shangin.). In Proceedings of the 3d Indian International Conference on Artificial
Intelligence (IICAI07), Puna,
India, Pages
12531266.
[29] Automated Natural Deduction for Propositional
Lineartime 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 915, 2007.
[30] Automating natural deduction for lineartime temporal logic (with O. Grigoriev and V.
Shangin.). In Proceedings of the
14th International Symposium on Temporal Representation and Reasoning, 2007.
TIME 2007, pages 4758,
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 14^{th} Workshop
on Automated Reasoning, (ARW
2007), Imperial
College, April 2007.
[33] Verification tool Grid component system (with A.Basso). The 14^{th} Workshop
on Automated Reasoning, (ARW
2007), Imperial
College, April 2007.
[34] Natural
Deduction Calculus For LinearTime Temporal Logic (with A. Basukoski, O. Grigoryev,
and V. Shangin). In Logics in
Artificial Intelligence, Proceedings
of 10^{th} European Conference (JELIA 2006), Volume 4160 of Lecture Notes in Computer Science, Liverpool,
September 2006, pages 5668.
[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 181186, Russian Academy of Sciences, Moscow, 1996. ISBN 5201019528.
[36]
Clausal Resolution for ECTL+: Complexity Analysis (with A.
Basukoski). Proceedings of IEEE
2006 John Vincent Atanasoff International Symposium
o Modern Computing, 36 October 2006, Sofia,
Bulgaria,
pages 16 (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 (IS2006),
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,
36 October 2006, Sofia, Bulgaria,
pages 175183.
[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 (IICAI05), Puna,
India, 2005,
pages 12921311.
[42]
Search
Strategies for Resolution in CTLType Logics: Extension and Complexity, (with A. Basukoski). Proceedings of the 12th International
Symposium on Temporal Representation and Reasoning, 2005. TIME 2005.
2325 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 140147.
[45] Proofsearching Algorithm in First Order Classical Natural
Deduction Calculus (with A. Bocharov, A.
Gorchakov and V. Shangin). Proceedings of 12^{th} International
Congress on Logic, Philosophy and Methodology of Science, Oviedo, August
2003.
[46] Clausal Resolution for Extended
Computation Tree Logic ECTL. Proceedings of the Time2003/ICTL2003
International Conference on Temporal Representation and
Reasoning/International Conference on Temporal Logic (Australia, July 2003), IEEE
Computer Society, 2003, pages 107117.
[47] Resolution for Branching Time
Temporal Logics. Smirnov's Readings. 4th
International Conference, Moscow,
2003.
[48] Clausal Resolution for Extended
Computation Tree Logic ECTL. 10^{th}
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 Time2000 International Conference
on Temporal Representation and Reasoning (Nova
Scotia, Canada,
July 2000), IEEE Computer Society, 2000, pages 163172.
[50] Resolution in a Logic of Rational
Agency (with C. Dixon  main contributor, and M. Fisher). Proceedings of the 14^{th}
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 1322.
[52] Automata on Infinite Words and
Temporal Logic Normal
Forms. 7^{th} 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
BranchingTime Logic (with M.
Fisher). Proceedings of the 11^{th}
International Congress of Logic, Methodology and Philosophy of Science
(Crakow, Poland, August 1999), pages 137148.
[55] Clausal Resolution for CTL* (with
C. Dixon, and M. Fisher) Mathematical
Foundations of Computer Science, Proceedings of the 24^{th}
International Symposium (MFCS'99), (Poland, August 1999), volume 1672 of
Lecture Notes in Computer Science, Springer, 1999, pages 137148.
[56] Clausal Resolution for
BranchingTime Temporal Logics and Temporal MuCalculus. 6^{th} Workshop on Automated
Reasoning, Edinburgh, 1999.
[57] A Resolution
Method for CTL BranchingTime Temporal Logic (with M. Fisher). Proceedings of the 4^{th}
International Workshop on Temporal Representation and Reasoning (TIME'97)
(Florida,
1997), IEEE Computer Society, pages 2027.
[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 12^{th}
International Philosophical Congress, Moscow, 1993 (in Russian).
[60] On Meyer's Reduction to 2nd Degree Formulae
and its Methodological Significance in Relevant Logic. Proceedings of the 10^{th}
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, ICICES2011,
S.A. Engineering
College, Chennai, 2324
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 MultiAgent Systems, March 1823, 2007.
T4. Natural Deduction
Calculus For Computation Tree Logic. 2006
John Vincent Atanasoff
International Symposium on Modern Computing,
36 October 2006, Sofia , Bulgaria.
T5. Formal Specification and Verification in
the BranchingTime 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 LinearTime
Temporal Mucalculus. Workshop on Fixpoint and FirstOrder Temporal
Logics. University
of Liverpool,
September, 2001.
T8. Clausal Resolution for Temporal
MuCalculus. 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 BranchingTime Temporal Logics. 1^{st} 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)
