David A. Plaisted
According to our database^{1},
David A. Plaisted
authored at least 98 papers
between 1972 and 2017.
Collaborative distances:
Collaborative distances:
Timeline
Legend:
Book In proceedings Article PhD thesis OtherLinks
Homepages:

at id.loc.gov

at isni.org

at dl.acm.org
On csauthors.net:
Bibliography
2017
SemanticallyGuided GoalSensitive Reasoning: Inference System and Completeness.
J. Autom. Reasoning, 2017
2016
SemanticallyGuided GoalSensitive Reasoning: Model Representation.
J. Autom. Reasoning, 2016
2015
History and Prospects for FirstOrder Automated Deduction.
Proceedings of the Automated Deduction  CADE25, 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 EUnification.
Appl. Algebra Eng. Commun. Comput., 2000
1999
Theory of PartialOrder 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 NonClassical Logics, 1998
1997
RRTP  A Replacement Rule Theorem Prover.
J. Autom. Reasoning, 1997
CLINS  A Semantically Guided FirstOrder 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 firstorder theorem proving.
Proceedings of the Satisfiability Problem: Theory and Applications, 1996
1995
A model for the parallel execution of subsetequational languages.
Future Generation Comp. Syst., 1995
Controlling the Consumption of Storage with Sliding Priority Search in a HyperLinking 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 InstanceBased 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  CADE12, 12th International Conference on Automated Deduction, Nancy, France, June 26, 1994
Semantically Guided FirstOrder Theorem Proving using HyperLinking.
Proceedings of the Automated Deduction  CADE12, 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 Instancebased 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 HyperLinking 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 FirstOrder Theorem Proving.
Proceedings of the Conditional Term Rewriting Systems, Third International Workshop, 1992
Proving Equality Theorems with HyperLinking.
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 SequentStyle Model Elimination Strategy and a Positive Refinement.
J. Autom. Reasoning, 1990
Rigid EUnification: NPCompleteness 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 DepthFirst IterativeDeepening 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
NonHorn Clause Logic Programming Without Contrapositives.
J. Autom. Reasoning, 1988
Rigid EUnification is NPComplete
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 StructurePreserving 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 MediumGrain 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 NonTermination Test for the KnuthBendix 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 AssociativeCommutative Rewriting Systems.
J. Symb. Comput., 1985
The Undecidability of SelfEmbedding 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 NPHard and NPComplete Polynomial and Integer Divisibility Problems.
Theor. Comput. Sci., 1984
Complete Problems in the FirstOrder Predicate Calculus.
J. Comput. Syst. Sci., 1984
Heuristic Matching for Graphs Satisfying the Triangle Inequality.
J. Algorithms, 1984
The OccurCheck 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
AssociativeCommutative 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 NPcomplete 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 NPHard.
SIAM J. Comput., 1978
1977
Sparse Complex Polynomials and Polynomial Reducibility.
J. Comput. Syst. Sci., 1977
New NPHard and NPComplete 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 NPHard
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