Deepak Kapur

Proceedings of the 6th International Conference on Formal Structures for Computation and Deduction, 2021

Interpolation and Amalgamation for Arrays with MaxDiff.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Software Science and Computation Structures, 2021

2020

Interpolation and Amalgamation for Arrays with MaxDiff (Extended Version).

[BibT_eX]

[DOI]

CoRR, 2020

An Algorithm for Computing a Minimal Comprehensive Gröbner\, Basis of a Parametric Polynomial System.

[BibT_eX]

[DOI]

Yiming Yang

CoRR, 2020

Compactly Representing Uniform Interpolants for EUF using (conditional) DAGS.

[BibT_eX]

[DOI]

CoRR, 2020

Computing Uniform Interpolants for EUF via (conditional) DAG-based Compact Representations.

[BibT_eX]

[DOI]

Proceedings of the 35th Italian Conference on Computational Logic, 2020

Deciding the Word Problem for Ground Identities with Commutative and Extensional Symbols.

[BibT_eX]

[DOI]

Franz Baader

Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020

2019

Conditional Congruence Closure over Uninterpreted and Interpreted Symbols.

[BibT_eX]

[DOI]

J. Syst. Sci. Complex., 2019

Editorial.

[BibT_eX]

[DOI]

Formal Aspects Comput., 2019

NIL: Learning Nonlinear Interpolants.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE 27, 2019

2018

An Efficient Algorithm for Computing Parametric Multivariate Polynomial GCD.

[BibT_eX]

[DOI]

Proceedings of the 2018 ACM on International Symposium on Symbolic and Algebraic Computation, 2018

2017

Comprehensive Gröbner basis theory for a parametric polynomial ideal and the associated completion algorithm.

[BibT_eX]

[DOI]

J. Syst. Sci. Complex., 2017

Preface - Special Issue of Selected Extended Papers of IJCAR 2014.

[BibT_eX]

[DOI]

Stéphane Demri

Christoph Weidenbach

J. Autom. Reason., 2017

Connecting Program Synthesis and Reachability: Automatic Program Repair Using Test-Input Generation.

[BibT_eX]

[DOI]

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

Nonlinear Polynomials, Interpolants and Invariant Generation for System Analysis.

[BibT_eX]

[DOI]

Proceedings of the 2nd International Workshop on Satisfiability Checking and Symbolic Computation co-located with the 42nd International Symposium on Symbolic and Algebraic Computation (ISSAC 2017), 2017

2016

Interpolation synthesis for quadratic polynomial inequalities and combination with \textit{EUF}.

[BibT_eX]

[DOI]

CoRR, 2016

Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF.

[BibT_eX]

[DOI]

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

2015

Decoding femininity in computer science in India.

[BibT_eX]

[DOI]

Roli Varma

Commun. ACM, 2015

An Algorithm to Check Whether a Basis of a Parametric Polynomial System is a Comprehensive Gröbner Basis and the Associated Completion Algorithm.

[BibT_eX]

[DOI]

Yiming Yang

Proceedings of the 2015 ACM on International Symposium on Symbolic and Algebraic Computation, 2015

Unification and Matching in Hierarchical Combinations of Syntactic Theories.

[BibT_eX]

[DOI]

Proceedings of the Frontiers of Combining Systems - 10th International Symposium, 2015

When Is a Formula a Loop Invariant?

[BibT_eX]

[DOI]

Proceedings of the Logic, Rewriting, and Concurrency, 2015

2014

DIG: A Dynamic Invariant Generator for Polynomial and Array Invariants.

[BibT_eX]

[DOI]

ACM Trans. Softw. Eng. Methodol., 2014

Hierarchical Combination of Matching Algorithms (Extended Abstract).

[BibT_eX]

[DOI]

Proceedings of the 28th International Workshop on Unification, 2014

On Asymmetric Unification and the Combination Problem in Disjoint Theories (Extended Abstract).

[BibT_eX]

[DOI]

Proceedings of the 28th International Workshop on Unification, 2014

An Abstract Domain to Infer Octagonal Constraints with Absolute Value.

[BibT_eX]

[DOI]

Proceedings of the Static Analysis - 21st International Symposium, 2014

Using dynamic analysis to generate disjunctive invariants.

[BibT_eX]

[DOI]

Proceedings of the 36th International Conference on Software Engineering, 2014

On Asymmetric Unification and the Combination Problem in Disjoint Theories.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Software Science and Computation Structures, 2014

2013

An efficient method for computing comprehensive Gröbner bases.

[BibT_eX]

[DOI]

J. Symb. Comput., 2013

An efficient algorithm for computing a comprehensive Gröbner system of a parametric polynomial system.

[BibT_eX]

[DOI]

J. Symb. Comput., 2013

On invariant checking.

[BibT_eX]

[DOI]

Zhihai Zhang

J. Syst. Sci. Complex., 2013

Synthesizing Switching Controllers for Hybrid Systems by Continuous Invariant Generation

[BibT_eX]

[DOI]

Naijun Zhan

Hengjun Zhao

CoRR, 2013

Hierarchical Combination of Unication Algorithms (Extended Abstract).

[BibT_eX]

[DOI]

Proceedings of the 27th International Workshop on Unification, 2013

Hierarchical Combination.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE-24, 2013

Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE-24, 2013

Synthesizing Switching Controllers for Hybrid Systems by Generating Invariants.

[BibT_eX]

[DOI]

Hengjun Zhao

Naijun Zhan

Proceedings of the Theories of Programming and Formal Methods, 2013

Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning and Mathematics, 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

Elimination Techniques for Program Analysis.

[BibT_eX]

[DOI]

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

2012

A brief introduction to Wen-Tsun Wu's academic career.

[BibT_eX]

[DOI]

Xiao-Shan Gao

J. Symb. Comput., 2012

Preface.

[BibT_eX]

[DOI]

Xiao-Shan Gao

J. Symb. Comput., 2012

Termination Analysis of Imperative Programs Using Bitvector Arithmetic.

[BibT_eX]

[DOI]

Carsten Sinz

Proceedings of the Verified Software: Theories, Tools, Experiments, 2012

Program Analysis Using Quantifier-Elimination Heuristics - (Extended Abstract).

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Models of Computation, 2012

Using dynamic analysis to discover polynomial and array invariants.

[BibT_eX]

[DOI]

Proceedings of the 34th International Conference on Software Engineering, 2012

A "Hybrid" Approach for Synthesizing Optimal Controllers of Hybrid Systems: A Case Study of the Oil Pump Industrial Example.

[BibT_eX]

[DOI]

Proceedings of the FM 2012: Formal Methods, 2012

Effective Symbolic Protocol Analysis via Equational Irreducibility Conditions.

[BibT_eX]

[DOI]

Proceedings of the Computer Security - ESORICS 2012, 2012

Rewriting Induction + Linear Arithmetic = Decision Procedure.

[BibT_eX]

[DOI]

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

2011

Unification over Distributive Exponentiation (Sub)Theories.

[BibT_eX]

[DOI]

J. Autom. Lang. Comb., 2011

Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis.

[BibT_eX]

[DOI]

Proceedings of the 25th International Workshop on Unification, 2011

Termination Analysis of C Programs Using Compiler Intermediate Languages.

[BibT_eX]

[DOI]

Carsten Sinz

Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, 2011

Protocol analysis in Maude-NPA using unification modulo homomorphic encryption.

[BibT_eX]

[DOI]

Proceedings of the 13th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2011

Computing comprehensive Gröbner systems and comprehensive Gröbner bases simultaneously.

[BibT_eX]

[DOI]

Proceedings of the Symbolic and Algebraic Computation, International Symposium, 2011

2010

Unification modulo a partial theory of exponentiation

[BibT_eX]

[DOI]

Andrew M. Marshall

Proceedings of the Proceedings 24th International Workshop on Unification, 2010

Shape Analysis with Reference Set Relations.

[BibT_eX]

[DOI]

Proceedings of the Verification, 2010

Idle Port Scanning and Non-interference Analysis of Network Protocol Stacks Using Model Checking.

[BibT_eX]

[DOI]

Proceedings of the 19th USENIX Security Symposium, 2010

Coverset Induction with Partiality and Subsorts: A Powerlist Case Study.

[BibT_eX]

[DOI]

Joe Hendrix

José Meseguer

Proceedings of the Interactive Theorem Proving, First International Conference, 2010

A new algorithm for computing comprehensive Gröbner systems.

[BibT_eX]

[DOI]

Proceedings of the Symbolic and Algebraic Computation, International Symposium, 2010

Induction, Invariants, and Abstraction.

[BibT_eX]

[DOI]

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

2009

An Algorithm for Computing a Gröbner Basis of a Polynomial Ideal over a Ring with Zero Divisors.

[BibT_eX]

[DOI]

Yongyang Cai

Math. Comput. Sci., 2009

Cayley-Dixon projection operator for multi-univariate composed polynomials.

[BibT_eX]

[DOI]

Manfred Minimair

J. Symb. Comput., 2009

Termination of Context-Sensitive Rewriting with Built-In Numbers and Collection Data Structures.

[BibT_eX]

[DOI]

Proceedings of the Functional and Constraint Logic Programming, 2009

Identification of logically related heap regions.

[BibT_eX]

[DOI]

Proceedings of the 8th International Symposium on Memory Management, 2009

A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 2009

2008

Operational Termination of Conditional Rewriting with Built-in Numbers and Semantic Data Structures.

[BibT_eX]

[DOI]

Proceedings of the 8th International Workshop on Reduction Strategies in Rewriting and Programming, 2008

Dependency Pairs for Rewriting with Built-In Numbers and Semantic Data Structures.

[BibT_eX]

[DOI]

Proceedings of the Rewriting Techniques and Applications, 19th International Conference, 2008

Sharing analysis of arrays, collections, and recursive structures.

[BibT_eX]

[DOI]

Mario Méndez-Lojo

Proceedings of the 8th ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering, 2008

Identification of Heap-Carried Data Dependence Via Explicit Store Heap Models.

[BibT_eX]

[DOI]

Proceedings of the Languages and Compilers for Parallel Computing, 2008

Efficient Context-Sensitive Shape Analysis with Graph Based Heap Models.

[BibT_eX]

[DOI]

Proceedings of the Compiler Construction, 17th International Conference, 2008

Multivariate Resultants in Bernstein Basis.

[BibT_eX]

[DOI]

Manfred Minimair

Proceedings of the Automated Deduction in Geometry - 7th International Workshop, 2008

2007

Automatic generation of polynomial invariants of bounded degree using abstract interpretation.

[BibT_eX]

[DOI]

Sci. Comput. Program., 2007

Generating all polynomial invariants in simple loops.

[BibT_eX]

[DOI]

J. Symb. Comput., 2007

Heap analysis in the presence of collection libraries.

[BibT_eX]

[DOI]

Proceedings of the 7th ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering, 2007

Dependency Pairs for Rewriting with Non-free Constructors.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 2007

2006

Preface on the contributed papers.

[BibT_eX]

[DOI]

J. Symb. Comput., 2006

Bruno Buchberger - A life devoted to symbolic computation.

[BibT_eX]

[DOI]

J. Symb. Comput., 2006

A Quantifier-Elimination Based Heuristic for Automatically Generating Inductive Assertions for Programs.

[BibT_eX]

[DOI]

J. Syst. Sci. Complex., 2006

Third Special Issue on Techniques for Automated Termination Proofs.

[BibT_eX]

[DOI]

J. Autom. Reason., 2006

Interpolation for data structures.

[BibT_eX]

[DOI]

Rupak Majumdar

Calogero G. Zarba

Proceedings of the 14th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2006

Inductive Decidability Using Implicit Induction.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2006

A Static Heap Analysis for Shape and Connectivity: Unified Memory Analysis: The Base Framework.

[BibT_eX]

[DOI]

Proceedings of the Languages and Compilers for Parallel Computing, 2006

Conditions for determinantal formula for resultant of a polynomial system.

[BibT_eX]

[DOI]

Proceedings of the Symbolic and Algebraic Computation, International Symposium, 2006

2005

Preface.

[BibT_eX]

[DOI]

J. Autom. Reason., 2005

Towards Dynamic Partitioning of Reactive System Behavior: A Train Controller Case Study.

[BibT_eX]

[DOI]

Victor L. Winter

Proceedings of the Reliable Systems on Unreliable Networked Platforms, 2005

Automatically Generating Loop Invariants Using Quantifier Elimination.

[BibT_eX]

[DOI]

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

Cayley-Dixon Resultant Matrices of Multi-univariate Composed Polynomials.

[BibT_eX]

[DOI]

Manfred Minimair

Proceedings of the Computer Algebra in Scientific Computing, 8th International Workshop, 2005

A Unification Algorithm for Analysis of Protocols with Blinded Signatures.

[BibT_eX]

[DOI]

Lida Wang

Proceedings of the Mechanizing Mathematical Reasoning, 2005

2004

Resultants for unmixed bivariate polynomial systems produced using the Dixon formulation.

[BibT_eX]

[DOI]

J. Symb. Comput., 2004

Constructing Sylvester-type resultant matrices using the Dixon formulation.

[BibT_eX]

[DOI]

J. Symb. Comput., 2004

Preface.

[BibT_eX]

[DOI]

Laurent Vigneron

J. Autom. Reason., 2004

Preface.

[BibT_eX]

[DOI]

J. Autom. Reason., 2004

An Abstract Interpretation Approach for Automatic Generation of Polynomial Invariants.

[BibT_eX]

[DOI]

Proceedings of the Static Analysis, 11th International Symposium, 2004

Automatic generation of polynomial loop.

[BibT_eX]

[DOI]

Proceedings of the Symbolic and Algebraic Computation, 2004

Support hull: relating the cayley-dixon resultant constructions to the support of a polynomial system.

[BibT_eX]

[DOI]

Proceedings of the Symbolic and Algebraic Computation, 2004

Program Verification Using Automatic Generation of Invariants.

[BibT_eX]

[DOI]

Proceedings of the Theoretical Aspects of Computing, 2004

Formal Specifcation and Refinement of a Safe Train Control Function.

[BibT_eX]

[DOI]

Victor L. Winter

G. Fuehrer

Proceedings of the Formal Methods for Embedded Distributed Systems, 2004

2003

Exact resultants for corner-cut unmixed multivariate polynomial systems using the Dixon formulation.

[BibT_eX]

[DOI]

J. Symb. Comput., 2003

Announcement.

[BibT_eX]

[DOI]

J. Autom. Reason., 2003

On the relationship between the Dixon-based resultant construction and the supports of polynomial systems.

[BibT_eX]

[DOI]

SIGSAM Bull., 2003

Automatic Generation of Generalization Lemmas for Proving Properties of Tail-Recursive Definitions.

[BibT_eX]

[DOI]

Nikita A. Sakhanenko

Proceedings of the Theorem Proving in Higher Order Logics, 16th International Conference, 2003

An E-unification Algorithm for Analyzing Protocols That Use Modular Exponentiation.

[BibT_eX]

[DOI]

Lida Wang

Proceedings of the Rewriting Techniques and Applications, 14th International Conference, 2003

Model Checking Reconfigurable Processor Configurations for Safety Properties.

[BibT_eX]

[DOI]

John Cochran

Proceedings of the Field Programmable Logic and Application, 13th International Conference, 2003

Deciding Inductive Validity of Equations.

[BibT_eX]

[DOI]

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

Automatic Generation of Simple Lemmas from Recursive Definitions Using Decision Procedures - Preliminary Report.

[BibT_eX]

[DOI]

Proceedings of the Advances in Computing Science, 2003

2002

On the efficiency and optimality of Dixon-based resultant methods.

[BibT_eX]

[DOI]

Proceedings of the Symbolic and Algebraic Computation, 2002

A Rewrite Rule Based Framework for Combining Decision Procedures.

[BibT_eX]

[DOI]

Proceedings of the Frontiers of Combining Systems, 4th International Workshop, 2002

2001

Designing a Controller for a Multi-Train Multi-Track System.

[BibT_eX]

[DOI]

Victor L. Winter

Raymond Berg

Proceedings of the Workshop on Algorithmic MeThods and Models for Optimization of RailwayS, 2001

Dependency Pairs for Equational Rewriting.

[BibT_eX]

[DOI]

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

A Survey: Applying Formal Methods to a Software Intensive System.

[BibT_eX]

[DOI]

Isabelle Vernier-Mounier

Proceedings of the 6th IEEE International Symposium on High-Assurance Systems Engineering (HASE 2001), 2001

Decidable Classes of Inductive Theorems.

[BibT_eX]

[DOI]

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

Rewriting, Induction and Decision Procedures: A Case Study of Presburger Arithmetic.

[BibT_eX]

[DOI]

Proceedings of the Symbolic Algebraic Methods and Verification Methods, 2001

2000

Using an induction prover for verifying arithmetic circuits.

[BibT_eX]

[DOI]

Int. J. Softw. Tools Technol. Transf., 2000

Conditions for exact resultants using the Dixon formulation.

[BibT_eX]

[DOI]

Proceedings of the 2000 International Symposium on Symbolic and Algebraic Computation, 2000

Extending Decision Procedures with Induction Schemes.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 2000

1998

Transformational Methodology for Proving Termination of Logic Programs.

[BibT_eX]

[DOI]

M. R. K. Krishna Rao

J. Log. Program., 1998

Mechanical Verification of Adder Circuits using Rewrite Rule Laboratory.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 1998

Geometric, Algebraic, and Thermophysical Techniques for Object Recognition in IR Imagery.

[BibT_eX]

[DOI]

Comput. Vis. Image Underst., 1998

Proving Associative-Communicative Termination Using RPO-Compatible Orderings.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction in Classical and Non-Classical Logics, 1998

IBDL: A Language for Interface Behavior Specification and Testing.

[BibT_eX]

[DOI]

Sreenivasa Viswanadha

Proceedings of the 4th USENIX Conference on Object-Oriented Technologies and Systems (COOTS), 1998

Mechanizing Reasoning about Large Finite Tables in a Rewrite Based Theorem Prover.

[BibT_eX]

[DOI]

Proceedings of the Advances in Computing Science, 1998

1997

Proving Termination of GHC Programs.

[BibT_eX]

[DOI]

M. R. K. Krishna Rao

New Gener. Comput., 1997

Rewriting, Decision Procedures and Lemma Speculation for Automated Hardware Verification.

[BibT_eX]

[DOI]

Proceedings of the Theorem Proving in Higher Order Logics, 10th International Conference, 1997

A Total, Ground path Ordering for Proving Termination of AC-Rewrite Systems.

[BibT_eX]

[DOI]

Proceedings of the Rewriting Techniques and Applications, 8th International Conference, 1997

Shostak's Congruence Closure as Completion.

[BibT_eX]

[DOI]

Proceedings of the Rewriting Techniques and Applications, 8th International Conference, 1997

Extraneous Factors in the Dixon Resultant Formulation.

[BibT_eX]

[DOI]

Proceedings of the 1997 International Symposium on Symbolic and Algebraic Computation, 1997

Synthesizing Controllers for Hybrid Systems.

[BibT_eX]

[DOI]

Proceedings of the Hybrid and Real-Time Systems, 1997

Mechanizing Verification of Arithmetic Circuits: SRT Division.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 1997

1996

New Uses of Linear Arithmetic in Automated Theorem Proving by Induction.

[BibT_eX]

[DOI]

J. Autom. Reason., 1996

Sparsity Considerations in Dixon Resultants.

[BibT_eX]

[DOI]

Proceedings of the Twenty-Eighth Annual ACM Symposium on the Theory of Computing, 1996

Distributed Larch Prover (DLP): An Experiment in Parallelizing a Rewrite-Rule Based Prover.

[BibT_eX]

[DOI]

Mark T. Vandevoorde

Proceedings of the Rewriting Techniques and Applications, 7th International Conference, 1996

Rewrite-Based Automated Reasoning: Challenges Ahead.

[BibT_eX]

[DOI]

Proceedings of the Rewriting Techniques and Applications, 7th International Conference, 1996

Automating Proofs of Integrity Constraints in Situation Calculus.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Intelligent Systems, 9th International Symposium, 1996

Parallel User Interfaces for Parallel Applications.

[BibT_eX]

[DOI]

Mark T. Vandevoorde

Proceedings of the 5th International Symposium on High Performance Distributed Computing (HPDC '96), 1996

Mechanically Verifying a Family of Multiplier Circuits.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 8th International Conference, 1996

Lemma Discovery in Automated Induction.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE-13, 13th International Conference on Automated Deduction, New Brunswick, NJ, USA, July 30, 1996

Automating Induction over Mutually Recursive Functions.

[BibT_eX]

[DOI]

Proceedings of the Algebraic Methodology and Software Technology, 1996

Automated Geometric Reasoning: Dixon Resultants, Gröbner Bases, and Characteristic Sets.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction in Geometry, 1996

Using Elimination Methods to Compute Thermophysical Algebraic Invariants from Infrared Imagery.

[BibT_eX]

[DOI]

Proceedings of the Thirteenth National Conference on Artificial Intelligence and Eighth Innovative Applications of Artificial Intelligence Conference, 1996

1995

A Path Ordering for Proving Termination of AC Rewrite Systems.

[BibT_eX]

[DOI]

J. Autom. Reason., 1995

Comparison of Various Multivariate Resultant Formulations.

[BibT_eX]

[DOI]

Proceedings of the 1995 International Symposium on Symbolic and Algebraic Computation, 1995

Maximal Extensions os Simplification Orderings.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 1995

Automated Reasoning About Parallel Algorithms Using Powerlists.

[BibT_eX]

[DOI]

Proceedings of the Algebraic Methodology and Software Technology, 1995

1994

An Overview of the Tecton Proof System.

[BibT_eX]

[DOI]

Xumin Nie

Theor. Comput. Sci., 1994

An Automated Tool for Analyzing Completeness of Equational Specifications.

[BibT_eX]

[DOI]

Proceedings of the 1994 International Symposium on Software Testing and Analysis, 1994

Algebraic and Geometric Reasoning Using Dixon Resultants.

[BibT_eX]

[DOI]

Lu Yang

Proceedings of the International Symposium on Symbolic and Algebraic Computation, 1994

Using Linear Arithmetic Procedure for Generating Induction Schemes.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 1994

1992

Complexity of Unification Problems with Associative-Commutative Operators.

[BibT_eX]

[DOI]

J. Autom. Reason., 1992

Double-exponential Complexity of Computing a Complete Set of AC-Unifiers

[BibT_eX]

[DOI]

Proceedings of the Seventh Annual Symposium on Logic in Computer Science (LICS '92), 1992

The Tecton Proof System.

[BibT_eX]

Xumin Nie

Proceedings of the Formal Methods in Databases and Software Engineering, 1992

Rewriting Concepts in the Study of Termination of Logic Programs.

[BibT_eX]

[DOI]

M. R. K. Krishna Rao

Proceedings of the ALPUK92, Proceedings of the 4th UK Conference on Logic Programming, London, 30 March, 1992

1991

Semi-Unification.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 1991

Automating Inductionless Induction Using Test Sets.

[BibT_eX]

[DOI]

J. Symb. Comput., 1991

Sufficient-Completeness, Ground-Reducibility and their Complexity.

[BibT_eX]

[DOI]

Daniel J. Rosenkrantz

Acta Informatica, 1991

The Tecton Proof System.

[BibT_eX]

[DOI]

Proceedings of the Rewriting Techniques and Applications, 4th International Conference, 1991

Modeling generic polyhedral objects with constraints.

[BibT_eX]

[DOI]

Van-Duc Nguyen

Joseph L. Mundy

Proceedings of the IEEE Computer Society Conference on Computer Vision and Pattern Recognition, 1991

A Case Study of the Completion Procedure: Proving Ring Commutativity Problems.

[BibT_eX]

Proceedings of the Computational Logic - Essays in Honor of Alan Robinson, 1991

1990

On Ground-Confluence of Term Rewriting Systems

[BibT_eX]

[DOI]

Friedrich Otto

Inf. Comput., May, 1990

Unnecessary Inferences in Associative-Commutative Completion Procedures.

[BibT_eX]

[DOI]

Math. Syst. Theory, 1990

Inference Rules and Proof Procedures for Inequations.

[BibT_eX]

[DOI]

Chilukuri K. Mohan

J. Log. Program., 1990

Refutational Proofs of Geometry Theorems via Characteristic Set Computation.

[BibT_eX]

[DOI]

H. K. Wan

Proceedings of the International Symposium on Symbolic and Algebraic Computation, 1990

A New Method for Proving Termination of AC-Rewrite Systems.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 1990

1989

Consider Only General Superpositions in Completion Procedures.

[BibT_eX]

[DOI]

Proceedings of the Rewriting Techniques and Applications, 3rd International Conference, 1989

An Overview of Rewrite Rule Laboratory (RRL).

[BibT_eX]

[DOI]

Proceedings of the Rewriting Techniques and Applications, 3rd International Conference, 1989

A Completion Procedure for Computing a Canonical Basis for a k-Subalgebra.

[BibT_eX]

[DOI]

Klaus Madlener

Proceedings of the Computers and Mathematics, 1989

1988

Computability and Implementability Issues in Abstract Data Types.

[BibT_eX]

[DOI]

Sci. Comput. Program., 1988

Only Prime Superpositions Need be Considered in the Knuth-Bendix Completion Procedure.

[BibT_eX]

[DOI]

J. Symb. Comput., 1988

Computing a Gröbner Basis of a Polynomial Ideal over a Euclidean Domain.

[BibT_eX]

[DOI]

Abdelilah Kandri-Rody

J. Symb. Comput., 1988

Proving Equivalence of Different Axiomatizations of Free Groups.

[BibT_eX]

[DOI]

J. Autom. Reason., 1988

Opening the AC-Unification Race.

[BibT_eX]

[DOI]

J. Autom. Reason., 1988

Wu's Method and its Application to Perspective Viewing.

[BibT_eX]

[DOI]

Joseph L. Mundy

Artif. Intell., 1988

Geometric Reasoning and Artificial Intelligence: Introduction to the Special Volume.

[BibT_eX]

[DOI]

Joseph L. Mundy

Artif. Intell., 1988

A Refutational Approach to Geometry Theorem Proving.

[BibT_eX]

[DOI]

Artif. Intell., 1988

A Multi-Level Geometric Reasoning System for Vision.

[BibT_eX]

[DOI]

Artif. Intell., 1988

A Mechanizable Induction Principle for Equational Specifications.

[BibT_eX]

[DOI]

Proceedings of the 9th International Conference on Automated Deduction, 1988

First-Order Theorem Proving Using Conditional Rewrite Rules.

[BibT_eX]

[DOI]

Proceedings of the 9th International Conference on Automated Deduction, 1988

RRL: A Rewrite Rule Laboratory.

[BibT_eX]

[DOI]

Proceedings of the 9th International Conference on Automated Deduction, 1988

GEOMETER: A Theorem Prover for Algebraic Geometry.

[BibT_eX]

[DOI]

David Cyrluk

Richard M. Harris

Proceedings of the 9th International Conference on Automated Deduction, 1988

1987

Complexity of Matching Problems.

[BibT_eX]

[DOI]

Dan Benanav

J. Symb. Comput., 1987

Matching, unification and complexity.

[BibT_eX]

[DOI]

SIGSAM Bull., 1987

Proof by Consistency.

[BibT_eX]

[DOI]

Artif. Intell., 1987

On Sufficient-Completeness and Related Properties of Term Rewriting Systems.

[BibT_eX]

[DOI]

Acta Informatica, 1987

Reasoning in Systems of Equations and Inequations.

[BibT_eX]

[DOI]

Chilukuri K. Mohan

Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 1987

1986

Using Gröbner Bases to Reason About Geometry Problems.

[BibT_eX]

[DOI]

J. Symb. Comput., 1986

Inductive Reasoning with Incomplete Specifications (Preliminary Report)

[BibT_eX]

Proceedings of the Symposium on Logic in Computer Science (LICS '86), 1986

Geometry theorem proving using Hilbert's Nullstellensatz.

[BibT_eX]

[DOI]

Proceedings of the Symposium on Symbolic and Algebraic Manipulation, 1986

Complexity of Sufficient-Completeness.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 1986

RRL: A Rewrite Rule Laboratory.

[BibT_eX]

[DOI]

Proceedings of the 8th International Conference on Automated Deduction, Oxford, England, July 27, 1986

Proof by Induction Using Test Sets.

[BibT_eX]

[DOI]

Proceedings of the 8th International Conference on Automated Deduction, Oxford, England, July 27, 1986

NP-Completeness of the Set Unification and Matching Problems.

[BibT_eX]

[DOI]

Proceedings of the 8th International Conference on Automated Deduction, Oxford, England, July 27, 1986

1985

The Church-Rosser Property and Special Thue Systems.

[BibT_eX]

[DOI]

Robert McNaughton

Theor. Comput. Sci., 1985

A Finite Thue System with Decidable Word Problem and without Equivalent Finite Canonical System.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 1985

An O(|T|3) Algorithm for Testing the Church-Rosser Property of Thue Systems.

[BibT_eX]

[DOI]

Robert McNaughton

Theor. Comput. Sci., 1985

RRL: theorem proving environment based on rewriting techniques.

[BibT_eX]

[DOI]

ACM SIGSOFT Softw. Eng. Notes, 1985

An equational approach to theorem proving in first-order predicate calculus.

[BibT_eX]

[DOI]

ACM SIGSOFT Softw. Eng. Notes, 1985

The Knuth-Bendix Completion Procedure and Thue Systems.

[BibT_eX]

[DOI]

SIAM J. Comput., 1985

Worst-Case Choice for the Stable Marriage Problem.

[BibT_eX]

[DOI]

Inf. Process. Lett., 1985

A Rewrite Rule Based Approach for Synthesizing Abstract Data Types.

[BibT_eX]

[DOI]

Proceedings of the Mathematical Foundations of Software Development, 1985

A Path Ordering for Proving Termination of Term Rewriting Systems.

[BibT_eX]

[DOI]

Proceedings of the Mathematical Foundations of Software Development, 1985

An Ideal-Theoretic Approach to Work Problems and Unification Problems over Finitely Presented Commutative Algebras.

[BibT_eX]

[DOI]

Abdelilah Kandri-Rody

Proceedings of the Rewriting Techniques and Applications, First International Conference, 1985

Reasoning about three dimensional space.

[BibT_eX]

[DOI]

Proceedings of the 1985 IEEE International Conference on Robotics and Automation, 1985

1984

Algorithms for Computing Groebner Bases of Polynomial Ideals over Various Euclidean Rings.

[BibT_eX]

[DOI]

Abdelilah Kandri-Rody

Proceedings of the EUROSAM 84, 1984

A Natural Proof System Based on rewriting Techniques.

[BibT_eX]

[DOI]

Balakrishnan Krishnamurthy

Proceedings of the 7th International Conference on Automated Deduction, 1984

1983

On Proving Uniform Termination and Restricted Termination of Rewriting Systems.

[BibT_eX]

[DOI]

John V. Guttag

SIAM J. Comput., 1983

1982

Derived Pairs, Overlap Closures, and Rewrite Dominoes: New Tools for Analyzing Term rewriting Systems.

[BibT_eX]

[DOI]

John V. Guttag

Proceedings of the Automata, 1982

Rewrite Rule Theory and Abstract Data Type Analysis.

[BibT_eX]

[DOI]

Proceedings of the Computer Algebra, 1982

1981

Operators and algebraic structures.

[BibT_eX]

[DOI]

Alexander A. Stepanov

Proceedings of the 1981 conference on Functional programming languages and computer architecture, 1981

Tecton: A Language for Manipulating Generic Objects.

[BibT_eX]

[DOI]

Alexander A. Stepanov

Proceedings of the Program Specification, 1981

1980

Expressiveness of the Operation Set of a Data Abstraction.

[BibT_eX]

[DOI]

Proceedings of the Conference Record of the Seventh Annual ACM Symposium on Principles of Programming Languages, 1980

1979

Specifications of Majster's traversable stack and Veloso's traversable stack.

[BibT_eX]

[DOI]