Publications by Anatoli Degtyarev

  1. Anatoli Degtyarev, Michael Fisher, and Boris Konev. Monodic Temporal Resolution. ACS Transactions in Computational logic, 7(1), 2006. (Paper)

  2. Vladimir Aleksic and Anatoli Degtyarev. On arbitrary selection strategy for basic superposition. In M. Fisher, W. van derv Hoek, B. Konev, and A. Lisitsa, editors, JELIA 2006,, Lecture Notes in Computer Science, Volume 4160, pages 20 - 28, Springer-Verlag, 2006. (Paper)

  3. Vladimir Aleksic and Anatoli Degtyarev. Regular Derivations in Basic Superposition-Based Calculi. In G. Sutcliffe and A. Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2005),, Lecture Notes in Computer Science, Volume 3835, pages 292 - 306, Springer-Verlag, December 2005. (Paper)

  4. Boris Konev, Anatoli Degtyarev, Clare Dixon, Michael Fisher and Ullrich Hustadt. Mechanising First-Order Temporal Resolution. Information and Computation, 199(1/2):55-86, 2005. (Paper)

  5. Anatoli Degtyarev, Robert Nieuwenhuis, and Andrei Voronkov. Stratified resolution. Journal of Symbolic Computation, 36(1/2):79-99, 2003. (Paper)

  6. Boris Konev, Anatoli Degtyarev, and Michael Fisher. Handling Equality in Monodic Temporal Resolution. In M. Vardi and A. Voronkov, editors, Logic for Programming and Automated Reasoning (LPAR 2003), Lecture Notes in Artificial Intelligence, volume 2850, Springer-Verlag, September 2003. (Paper)

  7. Anatoli Degtyarev, Michael Fisher, and Boris Konev. Monodic Temporal Resolution. In F. Baader, editor, Proceedings of CADE'19: International Conference on Automated Deduction, Lecture Notes in Computer Science, Springer-Verlag, 2003. (Paper)

  8. Boris Konev, Anatoli Degtyarev, Clare Dixon, Michael Fisher, and Ullrich Hustadt. Towards the Implementation of First-Order Temporal Resolution: the Finite Domain Case. In M. Reynolds and A. Sattar, editors, Proceedings of 10th International Symposium on Temporal Representation and Reasoning and Forth International Conference on Temporal Logic (TIME-ICTL 2003), IEEE Computer Society Press, pages 72-82, 2003. (Paper)

  9. Alexander Lyaletski, Konstantine Vershinine, Anatoli Degtyarev, and Andrey Paskevich. System of Automated Deduction (SAD): Linguistic and Deductive Pecularities. In M.A. Klopotek, S.T. Wierzchon, and M. Michaliwicz, editors, Advances in Soft Computing: Intelligent Information Systems 2002, pages 413-422, Physica-Verlag, Springer, 2002. (Paper)

  10. Anatoli Degtyarev, Michael Fisher, and Alexei Lisitsa. Equality and monodic first-order temporal logic. Studia Logica, 72(2), 2002. (Paper)

  11. James Brotherston, Anatoli Degtyarev, Michael Fisher, and Alexei Lisitsa. Searching for Invariants Using Temporal Resolution. In M. Baaz and A. Voronkov, editors, Logic for Programming and Automated Reasoning (LPAR 2002), Lecture Notes in Artificial Intelligence, volume 2514, pages 86-101, Springer-Verlag, September 2002. (Paper)

  12. Anatoli Degtyarev, Michael Fisher, and Boris Konev. A simplified clausal resolution procedure for propositional linear-time temporal logic. In C. Fermüller and U. Egly, editors, Proceedings of TABLEAUX 2002: Automated Reasoning with Tableaux and Related Methods, Lecture Notes in Computer Science, volume 2381, pages 85-99, Springer-Verlag, July 2002. (Paper)

  13. Anatoli Degtyarev and Andrei Voronkov. Kanger's Choices in Automated Reasoning. In G. Holmström-Hintikka, S. Linström, and R. Sliviski, editors, Collected papers of Stig Kanger with Essays on his Life and Work, volume II, Kluwer Academic Publisher, 2001. (Paper)

  14. Anatoli Degtyarev and Andrei Voronkov. The inverse method. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, volume 1, pages 179-272, Elsevier Science and MIT Press, 2001. (Paper)

  15. Anatoli Degtyarev and Andrei Voronkov. Equality reasoning in sequent-based methods. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, volume 1, pages 611-706, Elsevier Science, 2001. (Paper)

  16. Anatoli Degtyarev, Alexander Lyaletski, and Marina Morokhovets. On the EA-style integrated processing of self-contained mathematical texts. In M. Kerber and M. Kohlhase, editors, Symbolic Calculation and Automated Theorem Proving, pages 126-141, A K Peters, 2001. (Paper)

  17. Anatoli Degtyarev, Yuri Gurevich, and Andrei Voronkov. Herbrand's Theorem and Equational Reasoning: Problems and Solutions. In G. Paun, G. Rozenberg, and A. Salomaa, editors, Current Trends in Theoretical Computer Science: Entering the 21st Century, pages 303-326, World Scientific, 2001. (Paper)

  18. Anatoli Degtyarev and Michael Fisher. Towards First-Order Temporal Resolution. In F. Baader, G. Brewka, and T. Eiter, editors, Proceedings of KI 2001: Advances in Artificial Intelligence, Lecture Notes in Computer Science, volume 2174, pages 18-32, Springer-Verlag, September 2001. (Paper)

  19. Anatoli Degtyarev and Andrei Voronkov. Stratified Resolution. In D. McAllester, editor, Proceedings of CADE'17: International Conference on Automated Deduction, Lecture Notes in Computer Science, volume 1831, pages 365-384, Springer-Verlag, June 2000. (Paper)

  20. Anatoli Degtyarev, Yuri Gurevich, Paliath Narendran, Margus Veanes, and Andrei Voronkov. Decidability and Complexity of Simultaneous Rigid E-Unification with One Variable and Related Results. Theoretical Computer Science, 243(1/2):167-184, 2000. (Paper)

  21. Anatoli Degtyarev, Alexander Lyaletski, and Marina Morokhovets. Evidence Algorithm and Sequent Logical Inference Search. In H. Ganzinger, D. McAllester, and A. Voronkov, editors, Logic for Programming and Automated Reasoning (LPAR'99), Lecture Notes in Computer Science, volume 1705, pages 44-61, Springer-Verlag, September 1999. (Paper)

  22. Anatoli Degtyarev and Andrei Voronkov. Handling equality in logic programs via basic folding. 1998. To appear in Journal of Symbolic Computation (minor revisions pending). (Paper)

  23. Anatoli Degtyarev and Andrei Voronkov. What you always wanted to know about rigid E-unification. Journal of Automated Reasoning, 20(1):47-80, February 1998. (Paper)

  24. Anatoli Degtyarev, Yuri Gurevich, Paliath Narendran, Margus Veanes, and Andrei Voronkov. Decidability and Complexity of Simultaneous Rigid E-Unification with One Variable and Related Results. In T. Nipkov, editor, Rewriting Techniques and Applications (RTA'98), Lecture Notes in Computer Science, volume 1379, pages 181-195, Springer-Verlag, January 1998. (Paper)

  25. Anatoli Degtyarev and Andrei Voronkov. A Note on Semantics of Logics Programs with Equality Based on Complete Sets of E-Unifiers. Journal of Logic Programming, 28(3):207-216, September 1996. (Paper)

  26. Anatoli Degtyarev and Andrei Voronkov. Simultaneous Rigid E-Unification is Undecidable. In H. Kleine Büning, editor, Computer Science Logic. 9th International Workshop, CSL'95, LNCS, volume 1092, pages 178-190, Paderborn, Germany, September 1995, 1996.

  27. Anatoli Degtyarev and Andrei Voronkov. Handling Equality in Logic Programs via Basic Folding. In R. Dyckhoff, H. Herre, and P. Schroeder-Heister, editors, Extensions of Logic Programming (5th International Workshop, ELP'96), LNCS, volume 1050, pages 119-136, Leipzig, Germany, March 1996. (Paper)

  28. Anatoli Degtyarev and Andrei Voronkov. The Undecidability of Simultaneous Rigid E-Unification. Theoretical Computer Science, 166(1-2):291-300, 1996. (Paper)

  29. Anatoli Degtyarev and Andrei Voronkov. What You Always Wanted to Know About Rigid E-Unification. In J.J. Alferes, L.M. Pereira, and E. Orlowska, editors, Logics in Artificial Intelligence. European Workshop, JELIA'96, LNAI, volume 1126, pages 50-69, Évora, Portugal, September/October 1996.

  30. Anatoli Degtyarev and Andrei Voronkov. Decidability Problems for the Prenex Fragment of Intuitionistic Logic. In Eleventh Annual IEEE Symposium on Logic in Computer Science (LICS'96), pages 503-512, IEEE, New Brunswick, NJ, July 1996. (Paper)

  31. Anatoli Degtyarev and Andrei Voronkov. Equality Elimination for the Tableau Method. In J. Calmet and C. Limongelli, editors, Design and Implementation of Symbolic Computation Systems. International Symposium, DISCO'96, LNCS, volume 1128, pages 46-60, Karlsruhe, Germany, September 1996. (Paper)

  32. Anatoli Degtyarev, Yuri Matiyasevich, and Andrei Voronkov. Simultaneous Rigid E-Unification and Related Algorithmic Problems. In Eleventh Annual IEEE Symposium on Logic in Computer Science (LICS'96), pages 494-502, IEEE, New Brunswick, NJ, July 1996.

  33. Anatoli Degtyarev, Yuri Gurevich, and Andrei Voronkov. Herbrand's Theorem and Equational Reasoning: Problems and Solutions. In Bulletin of the European Association for Theoretical Computer Science, volume 60, pages 78-95, October 1996. The "Logic in Computer Science" column.

  34. Anatoli Degtyarev and Andrei Voronkov. Equality Elimination for the Inverse Method and Extension Procedures. In C.S. Mellish, editor, Proceedings of the International Joint Conference on Artificial Intelligence (IJCAI), volume 1, pages 342-347, Montréal, August 1995. (Paper)

  35. Anatoli Degtyarev and Andrei Voronkov. General Connections via Equality Elimination. In M. De Glas and Z. Pawlak, editors, Second World Conference on the Fundamentals of Artificial Intelligence (WOCFAI-95), pages 109-120, Angkor, Paris, July 1995. (Paper)

  36. Anatoli Degtyarev and Andrei Voronkov. A New Procedural Interpretation of Horn Clauses with Equality. In Leon Sterling, editor, Proceedings of the Twelfth International Conference on Logic Programming, pages 565-579, MIT, 1995.