David A. Plaisted

According to our database1, David A. Plaisted authored at least 98 papers between 1972 and 2017.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

Homepages:

On csauthors.net:

Bibliography

2017
Semantically-Guided Goal-Sensitive Reasoning: Inference System and Completeness.
J. Autom. Reasoning, 2017

2016
Semantically-Guided Goal-Sensitive Reasoning: Model Representation.
J. Autom. Reasoning, 2016

2015
History and Prospects for First-Order Automated Deduction.
Proceedings of the Automated Deduction - CADE-25, 2015

2014
SGGS Theorem Proving: an Exposition.
Proceedings of the 4th Workshop on Practical Aspects of Automated Reasoning, 2014

2013
The Relative Power of Semantics and Unification.
Proceedings of the Programming Logics - Essays in Memory of Harald Ganzinger, 2013

2008
Knowledge Representation and Classical Logic.
Proceedings of the Handbook of Knowledge Representation, 2008

2005
The Space Efficiency of OSHL.
Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2005

2003
A satisfiability procedure for quantified Boolean formulae.
Discrete Applied Mathematics, 2003

A relevance restriction strategy for automated deduction.
Artif. Intell., 2003

2002
Ordered Semantic Hyper Tableaux.
J. Autom. Reasoning, 2002

2001
General Algorithms for Permutations in Equational Inference.
J. Autom. Reasoning, 2001

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

2000
Special Cases and Substitutes for Rigid E-Unification.
Appl. Algebra Eng. Commun. Comput., 2000

1999
Theory of Partial-Order Programming.
Sci. Comput. Program., 1999

The Complexity of Some Complementation Problems.
Inf. Process. Lett., 1999

1998
Automated Deduction Techniques for Classification in Description Logic Systems.
J. Autom. Reasoning, 1998

Replacement Rules with Definition Detection.
Proceedings of the Automated Deduction in Classical and Non-Classical Logics, 1998

1997
RRTP - A Replacement Rule Theorem Prover.
J. Autom. Reasoning, 1997

CLIN-S - A Semantically Guided First-Order Theorem Prover.
J. Autom. Reasoning, 1997

Equational Reasoning using AC Constraints.
Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence, 1997

Ordered Semantic Hyper Linking.
Proceedings of the Fourteenth National Conference on Artificial Intelligence and Ninth Innovative Applications of Artificial Intelligence Conference, 1997

1996
Proof Lengths for Equational Completion.
Inf. Comput., 1996

Propositional search efficiency and first-order theorem proving.
Proceedings of the Satisfiability Problem: Theory and Applications, 1996

1995
A model for the parallel execution of subset-equational languages.
Future Generation Comp. Syst., 1995

Controlling the Consumption of Storage with Sliding Priority Search in a Hyper-Linking Based Theorem Prover.
Computers and Artificial Intelligence, 1995

1994
Use of replace rules in theorem proving.
Meth. of Logic in CS, 1994

Correctness of Unification Without Occur Check in Prolog.
J. Log. Program., 1994

Model Finding in Semantically Guided Instance-Based Theorem Proving.
Fundam. Inform., 1994

Problem Solving by Searching for Models with a Theorem Prover.
Artif. Intell., 1994

The Search Efficiency of Theorem Proving Strategies.
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.
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.
J. Symb. Comput., 1993

An Algorithm for Finding Canonical Sets of Ground Rewrite Rules in Polynomial Time.
J. ACM, 1993

Polynomial Time Termination and Constraint Satisfaction Tests.
Proceedings of the Rewriting Techniques and Applications, 5th International Conference, 1993

Model Finding Strategies in Semantically Guided Instance-based Theorem Proving.
Proceedings of the Methodologies for Intelligent Systems, 7th International Symposium, 1993

Finding Logical Consequences Using Unskolemization.
Proceedings of the Methodologies for Intelligent Systems, 7th International Symposium, 1993

Rough Resolution: A Refinement of Resolution to Remove Large Literals.
Proceedings of the 11th National Conference on Artificial Intelligence. Washington, 1993

1992
Eliminating Duplication with the Hyper-Linking Strategy.
J. Autom. Reasoning, 1992

A Semantic Backward Chaining Proof System.
Artif. Intell., 1992

Use of Unit Clauses and Clause Splitting in Automatic Deduction.
Proceedings of the Computing and Information, 1992

Conditional Term Rewriting and First-Order Theorem Proving.
Proceedings of the Conditional Term Rewriting Systems, Third International Workshop, 1992

Proving Equality Theorems with Hyper-Linking.
Proceedings of the Automated Deduction, 1992

1991
Rewrite, Rewrite, Rewrite, Rewrite, Rewrite, . . .
Theor. Comput. Sci., 1991

Term Rewriting: Some Experimental Results.
J. Symb. Comput., 1991

1990
Experimental Results on Subgoal Reordering.
IEEE Trans. Computers, 1990

A Heuristic Algorithm for Small Separators in Arbitrary Graphs.
SIAM J. Comput., 1990

A Sequent-Style Model Elimination Strategy and a Positive Refinement.
J. Autom. Reasoning, 1990

Rigid E-Unification: NP-Completeness and Applications to Equational Matings
Inf. Comput., 1990

A Complete Semantic Back Chaining Proof System.
Proceedings of the 10th International Conference on Automated Deduction, 1990

1989
Refinements to Depth-First Iterative-Deepening Search in Automatic Theorem Proving.
Artif. Intell., 1989

Programming with Equations, Subsets, and Relations.
Proceedings of the Logic Programming, 1989

Infinite Normal Forms (Preliminary Version).
Proceedings of the Automata, Languages and Programming, 16th International Colloquium, 1989

1988
Non-Horn Clause Logic Programming Without Contrapositives.
J. Autom. Reasoning, 1988

Rigid E-Unification is NP-Complete
Proceedings of the Third Annual Symposium on Logic in Computer Science (LICS '88), 1988

Term Rewriting: Some Experimental Results.
Proceedings of the 9th International Conference on Automated Deduction, 1988

A Goal Directed Theorem Prover.
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.
Proceedings of the 9th International Conference on Automated Deduction, 1988

1987
A Heuristic Triangulation Algorithm.
J. Algorithms, 1987

Functional programming with sets.
Proceedings of the Functional Programming Languages and Computer Architecture, 1987

A Logic for Conditional Term Rewriting Systems.
Proceedings of the Conditional Term Rewriting Systems, 1987

1986
A Structure-Preserving Clause Form Translation.
J. Symb. Comput., 1986

A Decision Procedure for Combinations of Propositional Temporal Logic and Other Specialized Theories.
J. Autom. Reasoning, 1986

The Denotional Semantics of Nondeterministic Recursive Programs using Coherent Relations
Proceedings of the Symposium on Logic in Computer Science (LICS '86), 1986

A Multiprocessor Architecture for Medium-Grain Parallelism.
Proceedings of the 6th International Conference on Distributed Computing Systems, 1986

Abstraction Using Generalization Functions.
Proceedings of the 8th International Conference on Automated Deduction, Oxford, England, July 27, 1986

A Simple Non-Termination Test for the Knuth-Bendix Method.
Proceedings of the 8th International Conference on Automated Deduction, Oxford, England, July 27, 1986

The Illinois Prover: A General Purpose Resolution Theorem Prover.
Proceedings of the 8th International Conference on Automated Deduction, Oxford, England, July 27, 1986

1985
Complete Divisibility Problems for Slowly Utilized Oracles.
Theor. Comput. Sci., 1985

Termination Orderings for Associative-Commutative Rewriting Systems.
J. Symb. Comput., 1985

The Undecidability of Self-Embedding for Term Rewriting Systems.
Inf. Process. Lett., 1985

Semantic Confluence Tests and Completion Methods
Information and Control, 1985

Logic Programming cum Applicative Programming.
Proceedings of the 1985 Symposium on Logic Programming, 1985

Associative Path Orderings.
Proceedings of the Rewriting Techniques and Applications, First International Conference, 1985

An Architecture for fast Data Movement in the FFP Machine.
Proceedings of the Functional Programming Languages and Computer Architecture, 1985

1984
New NP-Hard and NP-Complete Polynomial and Integer Divisibility Problems.
Theor. Comput. Sci., 1984

Complete Problems in the First-Order Predicate Calculus.
J. Comput. Syst. Sci., 1984

Heuristic Matching for Graphs Satisfying the Triangle Inequality.
J. Algorithms, 1984

The Occur-Check Problem in Prolog.
Proceedings of the 1984 International Symposium on Logic Programming, 1984

An Efficient Bug Location Algorithm.
Proceedings of the Second International Logic Programming Conference, 1984

Using Examples, Case Analysis, and Dependency Graphs in Theorem Proving.
Proceedings of the 7th International Conference on Automated Deduction, 1984

1983
The Travelling Salesman Problem and Minimum Matching in the Unit Square.
SIAM J. Comput., 1983

A Low Level Language for Obtaining Decision Procedure for Classes of temporal Logics.
Proceedings of the Logics of Programs, 1983

Associative-Commutative Rewriting.
Proceedings of the 8th International Joint Conference on Artificial Intelligence. Karlsruhe, 1983

1982
A Simplified Problem Reduction Format.
Artif. Intell., 1982

Comparison of Natural Deduction and Locking Resolution Implementations.
Proceedings of the 6th Conference on Automated Deduction, 1982

1981
Theorem Proving with Abstraction.
Artif. Intell., 1981

1980
The Application of Multivariate Polynomials to Inference Rules and Partial Tests for Unsatisfiability.
SIAM J. Comput., 1980

An NP-complete matching problem.
Discrete Applied Mathematics, 1980

Heuristics for Weighted Perfect Matching
Proceedings of the 12th Annual ACM Symposium on Theory of Computing, 1980

On the Distribution of Independent Formulae of Number Theory
Proceedings of the 12th Annual ACM Symposium on Theory of Computing, 1980

Abstraction Mappings in Mechanical Theorem Proving.
Proceedings of the 5th Conference on Automated Deduction, 1980

An Efficient Relevance Criterion for Mechanical Theorem Proving.
Proceedings of the 1st Annual National Conference on Artificial Intelligence, 1980

1979
Fast Verification, Testing, and Generation of Large Primes.
Theor. Comput. Sci., 1979

1978
Some Polynomial and Integer Divisibility problems are NP-Hard.
SIAM J. Comput., 1978

1977
Sparse Complex Polynomials and Polynomial Reducibility.
J. Comput. Syst. Sci., 1977

New NP-Hard and NP-Complete Polynomial and Integer Divisibility Problems
Proceedings of the 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October, 1977

1976
Some Polynomial and Integer Divisibility Problems Are NP-Hard
Proceedings of the 17th Annual Symposium on Foundations of Computer Science, 1976

1972
Flowchart Schemata with Counters
Proceedings of the 4th Annual ACM Symposium on Theory of Computing, 1972


  Loading...