Consistency and Semantics of Equational Definitions over Predefined Algebras. - Valentin M. Antimirov; Anatoli Degtyarev (CTRS, 1992)

Consistency of Equational Enrichments. - Valentin M. Antimirov; Anatoli Degtyarev (LPAR, 1992)

Completeness of Equational Definitions over Predefined Algebras. - Valentin M. Antimirov; Anatoli Degtyarev (AMAST, 1993)

Simultaneous Regid E-Unification Is Undecidable. - Anatoli Degtyarev; Andrei Voronkov (CSL, 1995)

A New Procedural Interpretation of Horn Clauses with Equality. - Anatoli Degtyarev; Andrei Voronkov (ICLP, 1995)

Equality Elimination for the Inverse Method and Extension Procedures. - Anatoli Degtyarev; Andrei Voronkov (IJCAI, 1995)

General Connections via Equality Elimination. - Anatoli Degtyarev; Andrei Voronkov (WOCFAI, 1995)

Equality Elimination for the Tableau Method. - Anatoli Degtyarev; Andrei Voronkov (DISCO, 1996)

Handling Equality in Logic Programming via Basic Folding. - Anatoli Degtyarev; Andrei Voronkov (ELP, 1996)

Simultaneous E-Unification and Related Algorithmic Problems. - Anatoli Degtyarev; Yuri V. Matiyasevich; Andrei Voronkov (LICS, 1996)

Decidability Problems for the Prenex Fragment of Intuitionistic Logic. - Anatoli Degtyarev; Andrei Voronkov (LICS, 1996)

Herbrand's Theorem and Equational Reasoning: Problems and Solutions. - Anatoli Degtyarev; Yuri Gurevich; Andrei Voronkov (Bull. EATCS, 1996)

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

The Undecidability of Simultaneous Rigid E-Unification. - Anatoli Degtyarev; Andrei Voronkov (Theor. Comput. Sci., 1996)

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

What You Always Wanted to Know about Rigid E-Unification. - Anatoli Degtyarev; Andrei Voronkov (J. Autom. Reason., 1998)

Evidence Algorithm and Sequent Logical Inference Search. - Anatoli Degtyarev; Alexander V. Lyaletski; Marina K. Morokhovets (LPAR, 1999)

Propositional Temporal Resolution Revised. - Anatoli Degtyarev; Michael Fisher 001 (ARW, 2000)

Stratified Resolution. - Anatoli Degtyarev; Andrei Voronkov (CADE, 2000)

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

The Inverse Method. - Anatoli Degtyarev; Andrei Voronkov (Handbook of Automated Reasoning, 2001)

Equality Reasoning in Sequent-Based Calculi. - Anatoli Degtyarev; Andrei Voronkov (Handbook of Automated Reasoning, 2001)

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

Towards First-Order Temporal Resolution. - Anatoli Degtyarev; Michael Fisher 001 (KI/ÖGAI, 2001)

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

Searching for Invariants Using Temporal Resolution. - James Brotherston; Anatoli Degtyarev; Michael Fisher 001; Alexei Lisitsa 001 (LPAR, 2002)

A Simplified Clausal Resolution Procedure for Propositional Linear-Time Temporal Logic. - Anatoli Degtyarev; Michael Fisher 001; Boris Konev (TABLEAUX, 2002)

Equality and Monodic First-Order Temporal Logic. - Anatoli Degtyarev; Michael Fisher 001; Alexei Lisitsa 001 (Stud Logica, 2002)

Handling Equality in Monodic Temporal Resolution. - Boris Konev; Anatoli Degtyarev; Michael Fisher 001 (LPAR, 2003)

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

Stratified resolution. - Anatoli Degtyarev; Robert Nieuwenhuis; Andrei Voronkov (J. Symb. Comput., 2003)

Regular Derivations in Basic Superposition-Based Calculi. - Vladimir Aleksic; Anatoli Degtyarev (LPAR, 2005)

Mechanising first-order temporal resolution. - Boris Konev; Anatoli Degtyarev; Clare Dixon; Michael Fisher 001; Ullrich Hustadt (Inf. Comput., 2005)

On Arbitrary Selection Strategies for Basic Superposition. - Vladimir Aleksic; Anatoli Degtyarev (JELIA, 2006)

Monodic temporal resolution. - Anatoli Degtyarev; Michael Fisher 001; Boris Konev (ACM Trans. Comput. Log., 2006)

Access Control and Obligations in the Category-Based Metamodel: A Rewrite-Based Semantics. - Sandra Alves; Anatoli Degtyarev; Maribel Fernández (LOPSTR, 2014)