Anatoli Degtyarev

Anatoli Degtyarev, Michael Fisher, Boris Konev: Monodic temporal resolution. ACM Trans. Comput. Log. 7(1): 108-150 (2006)

Vladimir Aleksic, Anatoli Degtyarev: On Arbitrary Selection Strategies for Basic Superposition. JELIA 2006: 20-28

Boris Konev, Anatoli Degtyarev, Clare Dixon, Michael Fisher, Ullrich Hustadt: Mechanising first-order temporal resolution. Inf. Comput. 199(1-2): 55-86 (2005)

Vladimir Aleksic, Anatoli Degtyarev: Regular Derivations in Basic Superposition-Based Calculi. LPAR 2005: 292-306

Anatoli Degtyarev, Robert Nieuwenhuis, Andrei Voronkov: Stratified resolution. J. Symb. Comput. 36(1-2): 79-99 (2003)

Anatoli Degtyarev, Michael Fisher, Boris Konev: Monodic Temporal Resolution. CADE 2003: 397-411

Boris Konev, Anatoli Degtyarev, Michael Fisher: Handling Equality in Monodic Temporal Resolution. LPAR 2003: 214-228

Boris Konev, Anatoli Degtyarev, Clare Dixon, Michael Fisher, Ullrich Hustadt: Towards the Implementation of First-Order Temporal Resolution: the Expanding Domain Case. TIME 2003: 72-82

Anatoli Degtyarev, Michael Fisher, Boris Konev: Monodic temporal resolution. CoRR cs.LO/0306041 (2003)

Anatoli Degtyarev, Michael Fisher, Alexei Lisitsa: Equality and Monodic First-Order Temporal Logic. Studia Logica 72(2): 147-156 (2002)

Alexander V. Lyaletski, Konstantin Verchinine, Anatoli Degtyarev, Andrey Paskevich: System for Automated Deduction (SAD): Linguistic and Deductive Peculiarities. Intelligent Information Systems 2002: 413-422

James Brotherston, Anatoli Degtyarev, Michael Fisher, Alexei Lisitsa: Searching for Invariants Using Temporal Resolution. LPAR 2002: 86-101

Anatoli Degtyarev, Michael Fisher, Boris Konev: A Simplified Clausal Resolution Procedure for Propositional Linear-Time Temporal Logic. TABLEAUX 2002: 85-99

Anatoli Degtyarev, Andrei Voronkov: The Inverse Method. Handbook of Automated Reasoning 2001: 179-272

Anatoli Degtyarev, Andrei Voronkov: Equality Reasoning in Sequent-Based Calculi. Handbook of Automated Reasoning 2001: 611-706

Anatoli Degtyarev, Yuri Gurevich, Andrei Voronkov: Herbrand's Theorem and Equational Reasoning: Problems and Solutions. Current Trends in Theoretical Computer Science 2001: 303-326

Anatoli Degtyarev, Michael Fisher: Towards First-Order Temporal Resolution. KI/ÖGAI 2001: 18-32

Anatoli Degtyarev, Yuri Gurevich, Paliath Narendran, Margus Veanes, Andrei Voronkov: Decidability and complexity of simultaneous rigid E-unification with one variable and related results. Theor. Comput. Sci. 243(1-2): 167-184 (2000)

Anatoli Degtyarev, Andrei Voronkov: Stratified Resolution. CADE 2000: 365-384

Anatoli Degtyarev, Alexander V. Lyaletski, Marina K. Morokhovets: Evidence Algorithm and Sequent Logical Inference Search. LPAR 1999: 44-61

Anatoli Degtyarev, Andrei Voronkov: What You Always Wanted to Know about Rigid E-Unification. J. Autom. Reasoning 20(1): 47-80 (1998)

Anatoli Degtyarev, Yuri Gurevich, Paliath Narendran, Margus Veanes, Andrei Voronkov: The Decidability of Simultaneous Rigid E-Unification with One Variable. RTA 1998: 181-195

Anatoli Degtyarev, Yuri Gurevich, Andrei Voronkov: Herbrand's Theorem and Equational Reasoning: Problems and Solutions. Bulletin of the EATCS 60: 78-96 (1996)

Anatoli Degtyarev, Andrei Voronkov: A Note on Semantics of Logic Programs with Equality Based on Complete Sets of E-Unifiers. J. Log. Program. 28(3): 207-216 (1996)

Anatoli Degtyarev, Andrei Voronkov: The Undecidability of Simultaneous Rigid E-Unification. Theor. Comput. Sci. 166(1&2): 291-300 (1996)

Anatoli Degtyarev, Andrei Voronkov: Equality Elimination for the Tableau Method. DISCO 1996: 46-60

Anatoli Degtyarev, Andrei Voronkov: Handling Equality in Logic Programming via Basic Folding. ELP 1996: 119-136

Anatoli Degtyarev, Andrei Voronkov: What You Always Wanted to Know About Rigid E-Unification. JELIA 1996: 50-69

Anatoli Degtyarev, Yuri Matiyasevich, Andrei Voronkov: Simultaneous E-Unification and Related Algorithmic Problems. LICS 1996: 494-502

Anatoli Degtyarev, Andrei Voronkov: Decidability Problems for the Prenex Fragment of Intuitionistic Logic. LICS 1996: 503-512

Anatoli Degtyarev, Andrei Voronkov: Simultaneous Regid E-Unification Is Undecidable. CSL 1995: 178-190

Anatoli Degtyarev, Andrei Voronkov: A New Procedural Interpretation of Horn Clauses with Equality. ICLP 1995: 565-579

Anatoli Degtyarev, Andrei Voronkov: Equality Elimination for the Inverse Method and Extension Procedures. IJCAI 1995: 342-347

Anatoli Degtyarev, Andrei Voronkov: General Connections via Equality Elimination. WOCFAI 1995: 109-120

Valentin M. Antimirov, Anatoli Degtyarev: Completeness of Equational Definitions over Predefined Algebras. AMAST 1993: 377-384

Valentin M. Antimirov, Anatoli Degtyarev: Consistency and Semantics of Equational Definitions over Predefined Algebras. CTRS 1992: 67-81

Valentin M. Antimirov, Anatoli Degtyarev: Consistency of Equational Enrichments. LPAR 1992: 293-402