David A. Plaisted

Proceedings of the IEEE International Parallel and Distributed Processing Symposium, 2022

2021

Interactive Online Configurator via Boolean Satisfiability Modeling.

[BibT_eX]

[DOI]

Tao Tao

Proceedings of the IAIT 2021: The 12th International Conference on Advances in Information Technology, Bangkok, Thailand, 29 June 2021, 2021

Management of the TPTP Problem Set.

[BibT_eX]

[DOI]

Geoff Sutcliffe

Proceedings of the Third International Workshop on Automated Reasoning: Challenges, 2021

Relevance and Abstraction.

[BibT_eX]

[DOI]

Proceedings of the Third International Workshop on Automated Reasoning: Challenges, 2021

Search Spaces for Theorem Proving Strategies.

[BibT_eX]

[DOI]

Proceedings of the Third International Workshop on Automated Reasoning: Challenges, 2021

2020

A Term-Rewriting Semantics for Imperative Style Programming.

[BibT_eX]

[DOI]

Lee Barnett

CoRR, 2020

Situation Calculus by Term Rewriting.

[BibT_eX]

[DOI]

CoRR, 2020

2019

Properties and Extensions of Alternating Path Relevance - I.

[BibT_eX]

[DOI]

CoRR, 2019

The Aspect Calculus.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE 27, 2019

2017

Semantically-Guided Goal-Sensitive Reasoning: Inference System and Completeness.

[BibT_eX]

[DOI]

J. Autom. Reason., 2017

2016

Semantically-Guided Goal-Sensitive Reasoning: Model Representation.

[BibT_eX]

[DOI]

J. Autom. Reason., 2016

2015

History and Prospects for First-Order Automated Deduction.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE-25, 2015

2014

Constraint Manipulation in SGGS.

[BibT_eX]

[DOI]

Proceedings of the 28th International Workshop on Unification, 2014

SGGS Theorem Proving: an Exposition.

[BibT_eX]

[DOI]

Proceedings of the 4th Workshop on Practical Aspects of Automated Reasoning, 2014

2013

The Relative Power of Semantics and Unification.

[BibT_eX]

[DOI]

Swaha Miller

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

2008

Knowledge Representation and Classical Logic.

[BibT_eX]

[DOI]

Vladimir Lifschitz

Leora Morgenstern

Proceedings of the Handbook of Knowledge Representation, 2008

2005

The Space Efficiency of OSHL.

[BibT_eX]

[DOI]

Swaha Miller

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2005

2003

A satisfiability procedure for quantified Boolean formulae.

[BibT_eX]

[DOI]

Armin Biere

Discret. Appl. Math., 2003

An Abstract Programming System

[BibT_eX]

[DOI]

CoRR, 2003

A Hierarchical Situation Calculus

[BibT_eX]

[DOI]

CoRR, 2003

A relevance restriction strategy for automated deduction.

[BibT_eX]

[DOI]

Adnan H. Yahya

Artif. Intell., 2003

2002

Ordered Semantic Hyper Tableaux.

[BibT_eX]

[DOI]

Adnan H. Yahya

J. Autom. Reason., 2002

2001

General Algorithms for Permutations in Equational Inference.

[BibT_eX]

[DOI]

Jürgen Avenhaus

J. Autom. Reason., 2001

Rewriting.

[BibT_eX]

[DOI]

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

2000

Ordered Semantic Hyper-Linking.

[BibT_eX]

[DOI]

J. Autom. Reason., 2000

Special Cases and Substitutes for Rigid E-Unification.

[BibT_eX]

[DOI]

Appl. Algebra Eng. Commun. Comput., 2000

1999

Theory of Partial-Order Programming.

[BibT_eX]

[DOI]

Mauricio Osorio

Bharat Jayaraman

Sci. Comput. Program., 1999

The Complexity of Some Complementation Problems.

[BibT_eX]

[DOI]

Gregory Kucherov

Inf. Process. Lett., 1999

1998

Automated Deduction Techniques for Classification in Description Logic Systems.

[BibT_eX]

[DOI]

M. Paramasivam

J. Autom. Reason., 1998

Replacement Rules with Definition Detection.

[BibT_eX]

[DOI]

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

1997

RRTP - A Replacement Rule Theorem Prover.

[BibT_eX]

[DOI]

M. Paramasivam

J. Autom. Reason., 1997

CLIN-S - A Semantically Guided First-Order Theorem Prover.

[BibT_eX]

[DOI]

J. Autom. Reason., 1997

Equational Reasoning using AC Constraints.

[BibT_eX]

[DOI]

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

The efficiency of theorem proving strategies - a comparative and asymptotic analysis.

[BibT_eX]

Computational intelligence, Vieweg, ISBN: 978-3-528-05574-5, 1997

1996

Proof Lengths for Equational Completion.

[BibT_eX]

[DOI]

Andrea Sattler-Klein

Inf. Comput., 1996

Propositional search efficiency and first-order theorem proving.

[BibT_eX]

[DOI]

Geoffrey D. Alexander

Proceedings of the Satisfiability Problem: Theory and Applications, 1996

1995

A model for the parallel execution of subset-equational languages.

[BibT_eX]

[DOI]

Amos R. Omondi

Future Gener. Comput. Syst., 1995

Controlling the Consumption of Storage with Sliding Priority Search in a Hyper-Linking Based Theorem Prover.

[BibT_eX]

[DOI]

Comput. Artif. Intell., 1995

1994

Use of replace rules in theorem proving.

[BibT_eX]

[DOI]

Methods Log. Comput. Sci., 1994

Correctness of Unification Without Occur Check in Prolog.

[BibT_eX]

[DOI]

Ritu Chadha

J. Log. Program., 1994

Model Finding in Semantically Guided Instance-Based Theorem Proving.

[BibT_eX]

[DOI]

Fundam. Informaticae, 1994

Problem Solving by Searching for Models with a Theorem Prover.

[BibT_eX]

[DOI]

Artif. Intell., 1994

The Search Efficiency of Theorem Proving Strategies.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE-12, 12th International Conference on Automated Deduction, Nancy, France, June 26, 1994

Semantically Guided First-Order Theorem Proving using Hyper-Linking.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE-12, 12th International Conference on Automated Deduction, Nancy, France, June 26, 1994

1993

On the Mechanical Derivation of Loop Invariants.

[BibT_eX]

[DOI]

Ritu Chadha

J. Symb. Comput., 1993

An Algorithm for Finding Canonical Sets of Ground Rewrite Rules in Polynomial Time.

[BibT_eX]

[DOI]

J. ACM, 1993

Polynomial Time Termination and Constraint Satisfaction Tests.

[BibT_eX]

[DOI]

Proceedings of the Rewriting Techniques and Applications, 5th International Conference, 1993

Model Finding Strategies in Semantically Guided Instance-based Theorem Proving.

[BibT_eX]

[DOI]

Proceedings of the Methodologies for Intelligent Systems, 7th International Symposium, 1993

Finding Logical Consequences Using Unskolemization.

[BibT_eX]

[DOI]

Ritu Chadha

Proceedings of the Methodologies for Intelligent Systems, 7th International Symposium, 1993

Rough Resolution: A Refinement of Resolution to Remove Large Literals.

[BibT_eX]

[DOI]

Proceedings of the 11th National Conference on Artificial Intelligence. Washington, 1993

1992

Eliminating Duplication with the Hyper-Linking Strategy.

[BibT_eX]

[DOI]

J. Autom. Reason., 1992

A Semantic Backward Chaining Proof System.

[BibT_eX]

[DOI]

Artif. Intell., 1992

Use of Unit Clauses and Clause Splitting in Automatic Deduction.

[BibT_eX]

Proceedings of the Computing and Information, 1992

Conditional Term Rewriting and First-Order Theorem Proving.

[BibT_eX]

[DOI]

Geoffrey D. Alexander

Proceedings of the Conditional Term Rewriting Systems, Third International Workshop, 1992

Proving Equality Theorems with Hyper-Linking.

[BibT_eX]

[DOI]

Geoffrey D. Alexander

Proceedings of the Automated Deduction, 1992

1991

Rewrite, Rewrite, Rewrite, Rewrite, Rewrite, . . .

[BibT_eX]

[DOI]

Stéphane Kaplan

Theor. Comput. Sci., 1991

Term Rewriting: Some Experimental Results.

[BibT_eX]

[DOI]

Richard C. Potter

J. Symb. Comput., 1991

1990

Experimental Results on Subgoal Reordering.

[BibT_eX]

[DOI]

IEEE Trans. Computers, 1990

A Heuristic Algorithm for Small Separators in Arbitrary Graphs.

[BibT_eX]

[DOI]

SIAM J. Comput., 1990

A Sequent-Style Model Elimination Strategy and a Positive Refinement.

[BibT_eX]

[DOI]

J. Autom. Reason., 1990

Rigid E-Unification: NP-Completeness and Applications to Equational Matings

[BibT_eX]

[DOI]

Inf. Comput., 1990

A Complete Semantic Back Chaining Proof System.

[BibT_eX]

[DOI]

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

1989

Refinements to Depth-First Iterative-Deepening Search in Automatic Theorem Proving.

[BibT_eX]

[DOI]

Artif. Intell., 1989

Programming with Equations, Subsets, and Relations.

[BibT_eX]

Bharat Jayaraman

Proceedings of the Logic Programming, 1989

Infinite Normal Forms (Preliminary Version).

[BibT_eX]

[DOI]

Stéphane Kaplan

Proceedings of the Automata, Languages and Programming, 16th International Colloquium, 1989

1988

Non-Horn Clause Logic Programming Without Contrapositives.

[BibT_eX]

[DOI]

J. Autom. Reason., 1988

Rigid E-Unification is NP-Complete

[BibT_eX]

[DOI]

Proceedings of the Third Annual Symposium on Logic in Computer Science (LICS '88), 1988

A Goal Directed Theorem Prover.

[BibT_eX]

[DOI]

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

Finding Canonical Rewriting Systems Equivalent to a Finite Set of Ground Equations in Polynomial Time.

[BibT_eX]

[DOI]

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

1987

A Heuristic Triangulation Algorithm.

[BibT_eX]

[DOI]

Jiarong Hong

J. Algorithms, 1987

Functional programming with sets.

[BibT_eX]

[DOI]

Bharat Jayaraman

Proceedings of the Functional Programming Languages and Computer Architecture, 1987

A Logic for Conditional Term Rewriting Systems.

[BibT_eX]

[DOI]

Proceedings of the Conditional Term Rewriting Systems, 1987

1986

A Structure-Preserving Clause Form Translation.

[BibT_eX]

[DOI]

Steven Greenbaum

J. Symb. Comput., 1986

A Decision Procedure for Combinations of Propositional Temporal Logic and Other Specialized Theories.

[BibT_eX]

[DOI]

J. Autom. Reason., 1986

The Denotional Semantics of Nondeterministic Recursive Programs using Coherent Relations

[BibT_eX]

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

Extensions to functional programming in Scheme.

[BibT_eX]

[DOI]

J. W. Curry

Proceedings of the ACM SIGART International Symposium on Methodologies for Intelligent Systems, 1986

A Multiprocessor Architecture for Medium-Grain Parallelism.

[BibT_eX]

J. Dean Brock

Amos R. Omondi

Proceedings of the 6th International Conference on Distributed Computing Systems, 1986

Abstraction Using Generalization Functions.

[BibT_eX]

[DOI]

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

A Simple Non-Termination Test for the Knuth-Bendix Method.

[BibT_eX]

[DOI]

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

The Illinois Prover: A General Purpose Resolution Theorem Prover.

[BibT_eX]

[DOI]

Steven Greenbaum

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

1985

Complete Divisibility Problems for Slowly Utilized Oracles.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 1985

Conditional rewriting.

[BibT_eX]

[DOI]

ACM SIGSOFT Softw. Eng. Notes, 1985

Termination Orderings for Associative-Commutative Rewriting Systems.

[BibT_eX]

[DOI]

Leo Bachmair

J. Symb. Comput., 1985

The Undecidability of Self-Embedding for Term Rewriting Systems.

[BibT_eX]

[DOI]

Inf. Process. Lett., 1985

Semantic Confluence Tests and Completion Methods

[BibT_eX]

[DOI]

Inf. Control., 1985

Logic Programming cum Applicative Programming.

[BibT_eX]

Proceedings of the 1985 Symposium on Logic Programming, 1985

Associative Path Orderings.

[BibT_eX]

[DOI]

Leo Bachmair

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

An Architecture for fast Data Movement in the FFP Machine.

[BibT_eX]

[DOI]

Proceedings of the Functional Programming Languages and Computer Architecture, 1985

1984

New NP-Hard and NP-Complete Polynomial and Integer Divisibility Problems.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 1984

The Occur-Check Problem in Prolog.

[BibT_eX]

[DOI]

New Gener. Comput., 1984

Complete Problems in the First-Order Predicate Calculus.

[BibT_eX]

[DOI]

J. Comput. Syst. Sci., 1984

Heuristic Matching for Graphs Satisfying the Triangle Inequality.

[BibT_eX]

[DOI]

J. Algorithms, 1984

An Efficient Bug Location Algorithm.

[BibT_eX]

Proceedings of the Second International Logic Programming Conference, 1984

Using Examples, Case Analysis, and Dependency Graphs in Theorem Proving.

[BibT_eX]

[DOI]

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

1983

The Travelling Salesman Problem and Minimum Matching in the Unit Square.

[BibT_eX]

[DOI]

Kenneth J. Supowit

Edward M. Reingold

SIAM J. Comput., 1983

A Low Level Language for Obtaining Decision Procedure for Classes of temporal Logics.

[BibT_eX]

[DOI]

Proceedings of the Logics of Programs, 1983

Associative-Commutative Rewriting.

[BibT_eX]

[DOI]

Proceedings of the 8th International Joint Conference on Artificial Intelligence. Karlsruhe, 1983

1982

A Simplified Problem Reduction Format.

[BibT_eX]

[DOI]

Artif. Intell., 1982

Comparison of Natural Deduction and Locking Resolution Implementations.

[BibT_eX]

[DOI]

Proceedings of the 6th Conference on Automated Deduction, 1982

1981

Theorem Proving with Abstraction.

[BibT_eX]

[DOI]

Artif. Intell., 1981

1980

The Application of Multivariate Polynomials to Inference Rules and Partial Tests for Unsatisfiability.

[BibT_eX]

[DOI]

SIAM J. Comput., 1980

An NP-complete matching problem.

[BibT_eX]

[DOI]

Samuel Zaks

Discret. Appl. Math., 1980

Heuristics for Weighted Perfect Matching

[BibT_eX]

[DOI]

Kenneth J. Supowit

Edward M. Reingold

Proceedings of the 12th Annual ACM Symposium on Theory of Computing, 1980

On the Distribution of Independent Formulae of Number Theory

[BibT_eX]

[DOI]

Proceedings of the 12th Annual ACM Symposium on Theory of Computing, 1980

Abstraction Mappings in Mechanical Theorem Proving.

[BibT_eX]

[DOI]

Proceedings of the 5th Conference on Automated Deduction, 1980

An Efficient Relevance Criterion for Mechanical Theorem Proving.

[BibT_eX]

[DOI]

Proceedings of the 1st Annual National Conference on Artificial Intelligence, 1980

1979

Fast Verification, Testing, and Generation of Large Primes.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 1979

1978

Some Polynomial and Integer Divisibility problems are NP-Hard.

[BibT_eX]

[DOI]

SIAM J. Comput., 1978

1977

Sparse Complex Polynomials and Polynomial Reducibility.

[BibT_eX]

[DOI]

J. Comput. Syst. Sci., 1977

1976

Theorem proving and semantic trees.

[BibT_eX]

[DOI]

PhD thesis, 1976

1972

Flowchart Schemata with Counters

[BibT_eX]

[DOI]