Andrei Voronkov

Johannes Schoisswohl

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2021

Inductive Benchmarks for Automated Reasoning.

[BibT_eX]

[DOI]

Proceedings of the Intelligent Computer Mathematics - 14th International Conference, 2021

Induction with Recursive Definitions in Superposition.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer Aided Design, 2021

Integer Induction in Saturation.

[BibT_eX]

[DOI]

Petra Hozzová

Proceedings of the Automated Deduction - CADE 28, 2021

2020

Induction with Generalization in Superposition Reasoning.

[BibT_eX]

[DOI]

Proceedings of the Intelligent Computer Mathematics - 13th International Conference, 2020

2019

Induction in Saturation-Based Proof Search.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE 27, 2019

2018

Unification with Abstraction and Theory Instantiation in Saturation-Based Reasoning.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2018

Reasoning with Quantifiers and Theories Using Saturation-Based Reasoning.

[BibT_eX]

[DOI]

Proceedings of the 20th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2018

A FOOLish Encoding of the Next State Relations of Imperative Programs.

[BibT_eX]

[DOI]

Evgenii Kotelnikov

Proceedings of the Automated Reasoning - 9th International Joint Conference, 2018

2017

Testing a Saturation-Based Theorem Prover: Experiences and Challenges (Extended Version).

[BibT_eX]

[DOI]

CoRR, 2017

Testing a Saturation-Based Theorem Prover: Experiences and Challenges.

[BibT_eX]

[DOI]

Proceedings of the Tests and Proofs - 11th International Conference, 2017

Instantiation and Pretending to be an SMT Solver with Vampire.

[BibT_eX]

[DOI]

Proceedings of the 15th International Workshop on Satisfiability Modulo Theories affiliated with the International Conference on Computer-Aided Verification (CAV 2017), Heidelberg, Germany, July 22, 2017

Coming to terms with quantified reasoning.

[BibT_eX]

[DOI]

Simon Robillard

Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, 2017

First-Order Interpolation and Interpolating Proof Systems.

[BibT_eX]

[DOI]

Proceedings of the LPAR-21, 2017

2016

Finding Finite Models in Multi-sorted First-Order Logic.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2016, 2016

AVATAR Modulo Theories.

[BibT_eX]

[DOI]

Proceedings of the GCAI 2016. 2nd Global Conference on Artificial Intelligence, September 19, 2016

New Techniques in Clausal Form Generation.

[BibT_eX]

[DOI]

Proceedings of the GCAI 2016. 2nd Global Conference on Artificial Intelligence, September 19, 2016

A Clausal Normal Form Translation for FOOL.

[BibT_eX]

[DOI]

Proceedings of the GCAI 2016. 2nd Global Conference on Artificial Intelligence, September 19, 2016

The vampire and the FOOL.

[BibT_eX]

[DOI]

Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, 2016

Selecting the Selection.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 8th International Joint Conference, 2016

2015

A First Class Boolean Sort in First-Order Theorem Proving and TPTP.

[BibT_eX]

[DOI]

Evgenii Kotelnikov

Proceedings of the Intelligent Computer Mathematics - International Conference, 2015

Cooperating Proof Attempts.

[BibT_eX]

[DOI]

Dmitry Tishkovsky

Proceedings of the Automated Deduction - CADE-25, 2015

Playing with AVATAR.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE-25, 2015

2014

Experimenting with SAT Solvers in Vampire.

[BibT_eX]

[DOI]

Proceedings of the Human-Inspired Computing and Its Applications, 2014

Keynote talk: EasyChair.

[BibT_eX]

[DOI]

Proceedings of the ACM/IEEE International Conference on Automated Software Engineering, 2014

AVATAR: The Architecture for First-Order Theorem Provers.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 26th International Conference, 2014

The Challenges of Evaluating a New Feature in Vampire.

[BibT_eX]

[DOI]

Proceedings of the 1st and 2nd Vampire Workshops, Vampire@VSL 2014, 2014

SAT solving experiments in Vampire.

[BibT_eX]

[DOI]

Proceedings of the 1st and 2nd Vampire Workshops, Vampire@VSL 2014, 2014

Extensional Crisis and Proving Identity.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2014

2013

Bound Propagation for Arithmetic Reasoning in Vampire.

[BibT_eX]

[DOI]

Proceedings of the 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2013

The Inverse Method for Many-Valued Logics.

[BibT_eX]

[DOI]

Andrei Mantsivoda

Proceedings of the Advances in Artificial Intelligence and Its Applications, 2013

PDFX: fully-automated PDF-to-XML conversion of scientific literature.

[BibT_eX]

[DOI]

Alexandru Constantin

Steve Pettifer

Proceedings of the ACM Symposium on Document Engineering 2013, 2013

First-Order Theorem Proving and Vampire.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 25th International Conference, 2013

The 481 Ways to Split a Clause and Deal with Propositional Variables.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE-24, 2013

Planning with Effectively Propositional Logic.

[BibT_eX]

[DOI]

Proceedings of the Programming Logics - Essays in Memory of Harald Ganzinger, 2013

Harald Ganzinger's Legacy: Contributions to Logics and Programming.

[BibT_eX]

[DOI]

Proceedings of the Programming Logics - Essays in Memory of Harald Ganzinger, 2013

2012

Translating regular expression matching into transducers.

[BibT_eX]

[DOI]

Yuto Sakuma

Yasuhiko Minamide

J. Appl. Log., 2012

Playing in the grey area of proofs.

[BibT_eX]

[DOI]

Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2012

Preprocessing techniques for first-order clausification.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, 2012

EPR-Based Bounded Model Checking at Word Level.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 6th International Joint Conference, 2012

Vinter: A Vampire-Based Tool for Interpolation.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems - 10th Asian Symposium, 2012

2011

Decision Procedures in Soft, Hard and Bio-ware - Follow Up (Dagstuhl Seminar 11272).

[BibT_eX]

[DOI]

Dagstuhl Reports, 2011

Invariant Generation in Vampire.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2011

Case Studies on Invariant Generation Using a Saturation Theorem Prover.

[BibT_eX]

[DOI]

Proceedings of the Advances in Artificial Intelligence, 2011

GoRRiLA and Hard Reality.

[BibT_eX]

[DOI]

Proceedings of the Perspectives of Systems Informatics, 2011

Implementing Conflict Resolution.

[BibT_eX]

[DOI]

Nestan Tsiskaridze

Proceedings of the Perspectives of Systems Informatics, 2011

On Transfinite Knuth-Bendix Orders.

[BibT_eX]

[DOI]

Georg Moser

Proceedings of the Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31, 2011

Solving Systems of Linear Inequalities by Bound Propagation.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31, 2011

Sine Qua Non for Large Theory Reasoning.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31, 2011

2010

EasyChair.

[BibT_eX]

[DOI]

Proceedings of the 6th International Workshop on Automated Specification and Verification of Web Systems, 2010

Invariant and Type Inference for Matrices.

[BibT_eX]

[DOI]

Proceedings of the Verification, 2010

Evaluation of Automated Theorem Proving on the Mizar Mathematical Library.

[BibT_eX]

[DOI]

Josef Urban

Proceedings of the Mathematical Software, 2010

Encoding industrial hardware verification problems into effectively propositional logic.

[BibT_eX]

[DOI]

Proceedings of 10th International Conference on Formal Methods in Computer-Aided Design, 2010

10161 Executive Summary - Decision Procedures in Software, Hardware and Bioware.

[BibT_eX]

[DOI]

Proceedings of the Decision Procedures in Software, Hardware and Bioware, 18.04., 2010

10161 Abstracts Collection - Decision Procedures in Software, Hardware and Bioware.

[BibT_eX]

[DOI]

Proceedings of the Decision Procedures in Software, Hardware and Bioware, 18.04., 2010

Interpolation and Symbol Elimination in Vampire.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning, 5th International Joint Conference, 2010

2009

Path Feasibility Analysis for String-Manipulating Programs.

[BibT_eX]

[DOI]

Nikolaj S. Bjørner

Nikolai Tillmann

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2009

Satisfiability and Theories.

[BibT_eX]

[DOI]

Proceedings of the 11th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2009

Inter-program Properties.

[BibT_eX]

[DOI]

Iman Narasamdya

Proceedings of the Static Analysis, 16th International Symposium, 2009

Comparing Unification Algorithms in First-Order Theorem Proving.

[BibT_eX]

[DOI]

Proceedings of the KI 2009: Advances in Artificial Intelligence, 2009

Verifying equivalence of memories using a first order logic theorem prover.

[BibT_eX]

[DOI]

Zurab Khasidashvili

Mahmoud Kinanah

Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design, 2009

Finding Loop Invariants for Programs over Arrays Using a Theorem Prover.

[BibT_eX]

[DOI]

Proceedings of the Fundamental Approaches to Software Engineering, 2009

Conflict Resolution.

[BibT_eX]

[DOI]

Nestan Tsiskaridze

Proceedings of the Principles and Practice of Constraint Programming, 2009

Interpolation and Symbol Elimination.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 2009

2008

Proof Systems for Effectively Propositional Logic.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning, 4th International Joint Conference, 2008

2007

Encodings of Problems in Effectively Propositional Logic.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing, 2007

Integrating Linear Arithmetic into Superposition Calculus.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 21st International Workshop, 2007

Encodings of Bounded LTL Model Checking in Effectively Propositional Logic.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 2007

2006

Inconsistencies in Ontologies.

[BibT_eX]

[DOI]

Proceedings of the Logics in Artificial Intelligence, 10th European Conference, 2006

UNIDOOR: a Deductive Object-Oriented Database Management System.

[BibT_eX]

[DOI]

Mohammed K. Jaber

Proceedings of the 22nd International Conference on Data Engineering, 2006

Reasoning Support for Expressive Ontology Languages Using a Theorem Prover.

[BibT_eX]

[DOI]

Ian Horrocks

Proceedings of the Foundations of Information and Knowledge Systems, 2006

Implementation of UNIDOOR, a Deductive Object-Oriented Database System.

[BibT_eX]

[DOI]

Mohammed K. Jaber

Proceedings of the Advances in Databases and Information Systems, 2006

2005

Knuth-Bendix constraint solving is NP-complete.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2005

Efficient instance retrieval with standard and relational path indexing.

[BibT_eX]

[DOI]

Inf. Comput., 2005

Finding Basic Block and Variable Correspondence.

[BibT_eX]

[DOI]

Iman Narasamdya

Proceedings of the Static Analysis, 12th International Symposium, 2005

Random Databases and Threshold for Monotone Non-recursive Datalog.

[BibT_eX]

[DOI]

Proceedings of the Mathematical Foundations of Computer Science 2005, 2005

Basis of Solutions for a System of Linear Inequalities in Integers: Computation and Applications.

[BibT_eX]

[DOI]

Dimitri Chubarov

Proceedings of the Mathematical Foundations of Computer Science 2005, 2005

05431 Abstracts Collection - Deduction and Applications.

[BibT_eX]

[DOI]

Proceedings of the Deduction and Applications, 23.-28. October 2005, 2005

05431 Executive Summary - Deduction and Applications.

[BibT_eX]

[DOI]

Proceedings of the Deduction and Applications, 23.-28. October 2005, 2005

Solving First-Order Constraints over the Monadic Class.

[BibT_eX]

[DOI]

Dimitri Chubarov

Proceedings of the Mechanizing Mathematical Reasoning, 2005

Generation of Hard Non-Clausal Random Satisfiability Problems.

[BibT_eX]

[DOI]

Proceedings of the Proceedings, 2005

2004

Efficient Checking of Term Ordering Constraints.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - Second International Joint Conference, 2004

TeMP: A Temporal Monodic Prover.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - Second International Joint Conference, 2004

2003

Limited resource strategy in resolution theorem proving.

[BibT_eX]

[DOI]

J. Symb. Comput., 2003

Stratified resolution.

[BibT_eX]

[DOI]

Robert Nieuwenhuis

J. Symb. Comput., 2003

Proof-Search in Intuitionistic Logic with Equality, or Back to Simultaneous Rigid E-Unification.

[BibT_eX]

[DOI]

J. Autom. Reason., 2003

Orienting rewrite rules with the Knuth-Bendix order.

[BibT_eX]

[DOI]

Inf. Comput., 2003

Orienting Equalities with the Knuth-Bendix Order.

[BibT_eX]

[DOI]

Proceedings of the 18th IEEE Symposium on Logic in Computer Science (LICS 2003), 2003

Automated Reasoning: Past Story and New Trends.

[BibT_eX]

[DOI]

Proceedings of the IJCAI-03, 2003

Upper Bounds for a Theory of Queues.

[BibT_eX]

[DOI]

Proceedings of the Automata, Languages and Programming, 30th International Colloquium, 2003

A Logical Reconstruction of Reachability.

[BibT_eX]

[DOI]

Proceedings of the Perspectives of Systems Informatics, 2003

Fast Infinite-State Model Checking in Integer-Based Systems (Invited Lecture).

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 17th International Workshop, 2003

Complexity of Some Problems in Modal and Intuitionistic Calculi.

[BibT_eX]

[DOI]

Larisa Maksimova

Proceedings of the Computer Science Logic, 17th International Workshop, 2003

An AC-Compatible Knuth-Bendix Order.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE-19, 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28, 2003

2002

The design and implementation of VAMPIRE.

[BibT_eX]

[DOI]

AI Commun., 2002

The Decidability of the First-Order Theory of the Knuth-Bendix Order in the Case of Unary Signatures.

[BibT_eX]

[DOI]

Proceedings of the FST TCS 2002: Foundations of Software Technology and Theoretical Computer Science, 2002

First-Order Theorem Provers: the Next Generation.

[BibT_eX]

[DOI]

Proceedings of the 2002 International Workshop on Description Logics (DL2002), 2002

Using Canonical Representations of Solutions to Speed Up Infinite-State Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 14th International Conference, 2002

BRAIN : Backward Reachability Analysis with Integers.

[BibT_eX]

[DOI]

Proceedings of the Algebraic Methodology and Software Technology, 2002

2001

How to optimize proof-search in modal logics: new methods of proving redundancy criteria for sequent calculi.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2001

A decision procedure for term algebras with queues.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2001

Term-Modal Logics.

[BibT_eX]

[DOI]

Melvin Fitting

Lars Thalmann

Stud Logica, 2001

Complexity and expressive power of logic programming.

[BibT_eX]

[DOI]

ACM Comput. Surv., 2001

Verifying Orientability of Rewrite Rules Using the Knuth-Bendix Order.

[BibT_eX]

[DOI]

Proceedings of the Rewriting Techniques and Applications, 12th International Conference, 2001

Splitting Without Backtracking.

[BibT_eX]

Proceedings of the Seventeenth International Joint Conference on Artificial Intelligence, 2001

Adaptive Saturation-Based Reasoning.

[BibT_eX]

[DOI]

Proceedings of the Perspectives of System Informatics, 2001

Algorithms, Datastructures, and other Issues in Efficient Automated Deduction.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning, First International Joint Conference, 2001

Vampire 1.1 (System Description).

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning, First International Joint Conference, 2001

On the Evaluation of Indexing Techniques for Theorem Proving.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning, First International Joint Conference, 2001

Herbrand's Theorem and Equational Reasoning: Problems and Solutions.

[BibT_eX]

Proceedings of the Current Trends in Theoretical Computer Science, 2001

Preface.

[BibT_eX]

[DOI]

John Alan Robinson

Proceedings of the Handbook of Automated Reasoning (in 2 volumes), 2001

Term Indexing.

[BibT_eX]

[DOI]

I. V. Ramakrishnan

R. Sekar

Proceedings of the Handbook of Automated Reasoning (in 2 volumes), 2001

Equality Reasoning in Sequent-Based Calculi.

[BibT_eX]

[DOI]

Proceedings of the Handbook of Automated Reasoning (in 2 volumes), 2001

The Inverse Method.

[BibT_eX]

[DOI]

Proceedings of the Handbook of Automated Reasoning (in 2 volumes), 2001

2000

Decidability and complexity of simultaneous rigid E-unification with one variable and related results.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2000

Expressive Power and Data Complexity of Query Languages for Trees and Lists.

[BibT_eX]

[DOI]

Evgeny Dantsin

Proceedings of the Nineteenth ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems, 2000

How to Optimize Proof-Search in Modal Logics: A New Way of Proving Redundancy Criteria for Sequent Calculi.

[BibT_eX]

[DOI]

Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science, 2000

A Decision Procedure for the Existential Theory of Term Algebras with the Knuth-Bendix Ordering.

[BibT_eX]

[DOI]

Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science, 2000

Deciding K using inverse-K.

[BibT_eX]

Proceedings of the KR 2000, 2000

Partially Adaptive Code Trees.

[BibT_eX]

[DOI]

Proceedings of the Logics in Artificial Intelligence, European Workshop, 2000

Stratified Resolution.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 2000

System Description: Vampire 1.0.

[BibT_eX]

[DOI]

Proceedings of the Seventh Workshop on Automated Reasoning, 2000

The Existential Theories of Term Algebras with the Knuth-Bendix Orderings are Decidable.

[BibT_eX]

[DOI]

Proceedings of the Seventh Workshop on Automated Reasoning, 2000

1999

Simultaneous Rigid E-unification and other Decision Problems Related to the Herbrand Theorem.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 1999

Monadic Simultaneous Rigid E-unification.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 1999

The Ground-Negative Fragment of First-Order Logic Is Pip2-Complete.

[BibT_eX]

[DOI]

J. Symb. Log., 1999

A Nondeterministic Polynomial-Time Unification Algorithm for Bags, Sets and Trees.

[BibT_eX]

[DOI]

Evgeny Dantsin

Proceedings of the Foundations of Software Science and Computation Structure, 1999

KK: a theorem prover for K.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 1999

Vampire.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 1999

1998

Proof Search in Intuitionistic Logic with Equality, or Back to Simultaneous Rigid E-Unification.

[BibT_eX]

[DOI]

J. Autom. Reason., 1998

What You Always Wanted to Know about Rigid E-Unification.

[BibT_eX]

[DOI]

J. Autom. Reason., 1998

The Decidability of Simultaneous Rigid E-Unification with One Variable.

[BibT_eX]

[DOI]

Proceedings of the Rewriting Techniques and Applications, 9th International Conference, 1998

Complexity of Nonrecursive Logic Programs with Complex Values.

[BibT_eX]

[DOI]

Sergei G. Vorobyov

Proceedings of the Seventeenth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, 1998

Herbrand's Theorem, Automated Reasoning and Semantics Tableaux.

[BibT_eX]

[DOI]

Proceedings of the Thirteenth Annual IEEE Symposium on Logic in Computer Science, 1998

Elimination of Equality via Transformation with Ordering Constraints.

[BibT_eX]

[DOI]

Leo Bachmair

Harald Ganzinger

Proceedings of the Automated Deduction, 1998

1997

Complexity of Query Answering in Logic Databases with Complex Values.

[BibT_eX]

[DOI]

Evgeny Dantsin

Proceedings of the Logical Foundations of Computer Science, 4th International Symposium, 1997

Strategies in Rigid-Variable Methods.

[BibT_eX]

[DOI]

Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence, 1997

Monadic Simultaneous Rigid E-Unification and Related Problems.

[BibT_eX]

[DOI]

Proceedings of the Automata, Languages and Programming, 24th International Colloquium, 1997

1996

The Undecidability of Simultaneous Rigid E-Unification.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 1996

A Note on Semantics of Logic Programs with Equality Based on Complete Sets of E-Unifiers.

[BibT_eX]

[DOI]

J. Log. Program., 1996

Herbrand's Theorem and Equational Reasoning: Problems and Solutions.

[BibT_eX]

Bull. EATCS, 1996

Proof-Search in Intuitionistic Logic Based on Constraint Satisfaction.

[BibT_eX]

[DOI]

Proceedings of the Theorem Proving with Analytic Tableaux and Related Methods, 1996

Decidability Problems for the Prenex Fragment of Intuitionistic Logic.

[BibT_eX]

[DOI]

Proceedings of the Proceedings, 1996

Simultaneous E-Unification and Related Algorithmic Problems.

[BibT_eX]

[DOI]

Yuri V. Matiyasevich

Proceedings of the Proceedings, 1996

Merging Relational Database Technology with Constraint Technology.

[BibT_eX]

[DOI]

Proceedings of the Perspectives of System Informatics, 1996

Handling Equality in Logic Programming via Basic Folding.

[BibT_eX]

[DOI]

Proceedings of the Extensions of Logic Programming, 5th International Workshop, 1996

Semantics of Constraint Logic Programs with Bounded Quantifiers.

[BibT_eX]

[DOI]

Martin Argenius

Proceedings of the Extensions of Logic Programming, 5th International Workshop, 1996

Equality Elimination for the Tableau Method.

[BibT_eX]

[DOI]

Proceedings of the Design and Implementation of Symbolic Computation Systems, 1996

1995

The Anatomy of Vampire Implementing Bottom-up Procedures with Code Trees.

[BibT_eX]

[DOI]

J. Autom. Reason., 1995

On Computability by Logic Programs.

[BibT_eX]

[DOI]

Ann. Math. Artif. Intell., 1995

General Connections via Equality Elimination.

[BibT_eX]

Proceedings of the Second World Conference on the Fundamentals of Artificial Intelligence, 1995

Equality Elimination for the Inverse Method and Extension Procedures.

[BibT_eX]

[DOI]

Proceedings of the Fourteenth International Joint Conference on Artificial Intelligence, 1995

A New Procedural Interpretation of Horn Clauses with Equality.

[BibT_eX]

Proceedings of the Logic Programming, 1995

Simultaneous Regid E-Unification Is Undecidable.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 9th International Workshop, 1995

1994

An Implementation Technique for a Class of Bottom-Up Procedures.

[BibT_eX]

[DOI]

Proceedings of the Programming Language Implementation and Logic Programming, 1994

1993

A Construction of Typed Lambda Models Related to Feasible Computability.

[BibT_eX]

[DOI]

Vladimir Yu. Sazonov

Proceedings of the Computational Logic and Proof Theory, Third Kurt Gödel Colloquium, 1993

1992

Higher Order Functions in First Order Theory.

[BibT_eX]

[DOI]

Proceedings of the Theory of Computing and Systems, 1992

Theorem Proving in Non-Standard Logics Based on the Inverse Method.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 1992

1991

Declarative and Procedural Paradigms - Do they Really Compete? (Panel).

[BibT_eX]

[DOI]

Proceedings of the Processing Declarative Knowledge, 1991

Logic Programming with Bounded Quantifiers.

[BibT_eX]

[DOI]

Proceedings of the Logic Programming, First Russian Conference on Logic Programming, Irkutsk, Russia, September 14-18, 1990, 1991

On Completeness of Program Synthesis Systems.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 5th Workshop, 1991

1990

Towards the Theory of Programming in Constructive Logic.

[BibT_eX]

[DOI]

Proceedings of the ESOP'90, 1990

LISS - The Logic Inference Search System.

[BibT_eX]

[DOI]

Proceedings of the 10th International Conference on Automated Deduction, 1990

1988

A proof-search method for the first-order logic.

[BibT_eX]

[DOI]

Proceedings of the COLOG-88, 1988

On connections between classical and constructive semantics.

[BibT_eX]

[DOI]

Sergei Starchenko

Proceedings of the COLOG-88, 1988

1987

Deductive Program Synthesis and Markov's Principle.

[BibT_eX]

[DOI]