David A. Plaisted

Publication Activity (10 Years)

Years Active: 1972-2022
Publications (10 Years): 11

Top Venues

CoRR

ARCADE@CADE

CADE

J. Autom. Reason.

Publications

Tao Tao, David A. Plaisted
Automatic Parallelization of Programs via Software Stream Rewriting. IPDPS Workshops (2022)
David A. Plaisted
Relevance and Abstraction. ARCADE@CADE (2021)
Tao Tao, David A. Plaisted
Interactive Online Configurator via Boolean Satisfiability Modeling. IAIT (2021)
David A. Plaisted
Search Spaces for Theorem Proving Strategies. ARCADE@CADE (2021)
Geoff Sutcliffe, David A. Plaisted
Management of the TPTP Problem Set. ARCADE@CADE (2021)
David A. Plaisted, Lee Barnett
A Term-Rewriting Semantics for Imperative Style Programming. CoRR (2020)
David A. Plaisted
Situation Calculus by Term Rewriting. CoRR (2020)
David A. Plaisted
The Aspect Calculus. CADE (2019)
David A. Plaisted
Properties and Extensions of Alternating Path Relevance - I. CoRR (2019)
Maria Paola Bonacina, David A. Plaisted
Semantically-Guided Goal-Sensitive Reasoning: Inference System and Completeness. J. Autom. Reason. 59 (2) (2017)
Maria Paola Bonacina, David A. Plaisted
Semantically-Guided Goal-Sensitive Reasoning: Model Representation. J. Autom. Reason. 56 (2) (2016)
David A. Plaisted
History and Prospects for First-Order Automated Deduction. CADE (2015)
Maria Paola Bonacina, David A. Plaisted
SGGS Theorem Proving: an Exposition. PAAR@IJCAR (2014)
Maria Paola Bonacina, David A. Plaisted
Constraint Manipulation in SGGS. UNIF (2014)
David A. Plaisted, Swaha Miller
The Relative Power of Semantics and Unification. Programming Logics (2013)
Swaha Miller, David A. Plaisted
The Space Efficiency of OSHL. TABLEAUX (2005)
David A. Plaisted, Armin Biere, Yunshan Zhu
A satisfiability procedure for quantified Boolean formulae. Discret. Appl. Math. 130 (2) (2003)
David A. Plaisted
A Hierarchical Situation Calculus CoRR (2003)
David A. Plaisted
An Abstract Programming System CoRR (2003)
David A. Plaisted, Adnan H. Yahya
A relevance restriction strategy for automated deduction. Artif. Intell. 144 (1-2) (2003)
Adnan H. Yahya, David A. Plaisted
Ordered Semantic Hyper Tableaux. J. Autom. Reason. 29 (1) (2002)
Jürgen Avenhaus, David A. Plaisted
General Algorithms for Permutations in Equational Inference. J. Autom. Reason. 26 (3) (2001)
David A. Plaisted, Yunshan Zhu
Ordered Semantic Hyper-Linking. J. Autom. Reason. 25 (3) (2000)
David A. Plaisted
Special Cases and Substitutes for Rigid E-Unification. Appl. Algebra Eng. Commun. Comput. 10 (2) (2000)
Mauricio Osorio, Bharat Jayaraman, David A. Plaisted
Theory of Partial-Order Programming. Sci. Comput. Program. 34 (3) (1999)
David A. Plaisted, Gregory Kucherov
The Complexity of Some Complementation Problems. Inf. Process. Lett. 71 (3-4) (1999)
David A. Plaisted, Yunshan Zhu
Replacement Rules with Definition Detection. FTP (LNCS Selection) (1998)
M. Paramasivam, David A. Plaisted
Automated Deduction Techniques for Classification in Description Logic Systems. J. Autom. Reason. 20 (3) (1998)
David A. Plaisted, Yunshan Zhu
Equational Reasoning using AC Constraints. IJCAI (1) (1997)
M. Paramasivam, David A. Plaisted
RRTP - A Replacement Rule Theorem Prover. J. Autom. Reason. 18 (2) (1997)
David A. Plaisted, Yunshan Zhu
Ordered Semantic Hyper Linking. AAAI/IAAI (1997)
Heng Chu, David A. Plaisted
CLIN-S - A Semantically Guided First-Order Theorem Prover. J. Autom. Reason. 18 (2) (1997)
David A. Plaisted, Andrea Sattler-Klein
Proof Lengths for Equational Completion. Inf. Comput. 125 (2) (1996)
David A. Plaisted, Geoffrey D. Alexander
Propositional search efficiency and first-order theorem proving. Satisfiability Problem: Theory and Applications (1996)
Shie-Jue Lee, David A. Plaisted
Controlling the Consumption of Storage with Sliding Priority Search in a Hyper-Linking Based Theorem Prover. Comput. Artif. Intell. 14 (6) (1995)
Amos R. Omondi, David A. Plaisted
A model for the parallel execution of subset-equational languages. Future Gener. Comput. Syst. 11 (3) (1995)
Heng Chu, David A. Plaisted
Model Finding in Semantically Guided Instance-Based Theorem Proving. Fundam. Informaticae 21 (3) (1994)
Shie-Jue Lee, David A. Plaisted
Use of replace rules in theorem proving. Methods Log. Comput. Sci. 1 (2) (1994)
David A. Plaisted
The Search Efficiency of Theorem Proving Strategies. CADE (1994)
Ritu Chadha, David A. Plaisted
Correctness of Unification Without Occur Check in Prolog. J. Log. Program. 18 (2) (1994)
Shie-Jue Lee, David A. Plaisted
Problem Solving by Searching for Models with a Theorem Prover. Artif. Intell. 69 (1-2) (1994)
Heng Chu, David A. Plaisted
Semantically Guided First-Order Theorem Proving using Hyper-Linking. CADE (1994)
Ritu Chadha, David A. Plaisted
Finding Logical Consequences Using Unskolemization. ISMIS (1993)
Heng Chu, David A. Plaisted
Rough Resolution: A Refinement of Resolution to Remove Large Literals. AAAI (1993)
Jean H. Gallier, Paliath Narendran, David A. Plaisted, Stan Raatz, Wayne Snyder
An Algorithm for Finding Canonical Sets of Ground Rewrite Rules in Polynomial Time. J. ACM 40 (1) (1993)
Heng Chu, David A. Plaisted
Model Finding Strategies in Semantically Guided Instance-based Theorem Proving. ISMIS (1993)
David A. Plaisted
Polynomial Time Termination and Constraint Satisfaction Tests. RTA (1993)
Ritu Chadha, David A. Plaisted
On the Mechanical Derivation of Loop Invariants. J. Symb. Comput. 15 (5/6) (1993)
Xumin Nie, David A. Plaisted
A Semantic Backward Chaining Proof System. Artif. Intell. 55 (1) (1992)
David A. Plaisted, Geoffrey D. Alexander, Heng Chu, Shie-Jue Lee
Conditional Term Rewriting and First-Order Theorem Proving. CTRS (1992)
Geoffrey D. Alexander, David A. Plaisted
Proving Equality Theorems with Hyper-Linking. CADE (1992)
Shie-Jue Lee, David A. Plaisted
Use of Unit Clauses and Clause Splitting in Automatic Deduction. ICCI (1992)
Shie-Jue Lee, David A. Plaisted
Eliminating Duplication with the Hyper-Linking Strategy. J. Autom. Reason. 9 (1) (1992)
David A. Plaisted, Richard C. Potter
Term Rewriting: Some Experimental Results. J. Symb. Comput. 11 (1/2) (1991)
Nachum Dershowitz, Stéphane Kaplan, David A. Plaisted
Rewrite, Rewrite, Rewrite, Rewrite, Rewrite, . . . Theor. Comput. Sci. 83 (1) (1991)
Xumin Nie, David A. Plaisted
A Complete Semantic Back Chaining Proof System. CADE (1990)
Xumin Nie, David A. Plaisted
Experimental Results on Subgoal Reordering. IEEE Trans. Computers 39 (6) (1990)
David A. Plaisted
A Sequent-Style Model Elimination Strategy and a Positive Refinement. J. Autom. Reason. 6 (4) (1990)
David A. Plaisted
A Heuristic Algorithm for Small Separators in Arbitrary Graphs. SIAM J. Comput. 19 (2) (1990)
Jean H. Gallier, Paliath Narendran, David A. Plaisted, Wayne Snyder
Rigid E-Unification: NP-Completeness and Applications to Equational Matings Inf. Comput. 87 (1/2) (1990)
Xumin Nie, David A. Plaisted
Refinements to Depth-First Iterative-Deepening Search in Automatic Theorem Proving. Artif. Intell. 41 (2) (1989)
Nachum Dershowitz, Stéphane Kaplan, David A. Plaisted
Infinite Normal Forms (Preliminary Version). ICALP (1989)
Bharat Jayaraman, David A. Plaisted
Programming with Equations, Subsets, and Relations. NACLP (1989)
Jean H. Gallier, Wayne Snyder, Paliath Narendran, David A. Plaisted
Rigid E-Unification is NP-Complete LICS (1988)
David A. Plaisted
Non-Horn Clause Logic Programming Without Contrapositives. J. Autom. Reason. 4 (3) (1988)
Jean H. Gallier, Paliath Narendran, David A. Plaisted, Stan Raatz, Wayne Snyder
Finding Canonical Rewriting Systems Equivalent to a Finite Set of Ground Equations in Polynomial Time. CADE (1988)
Richard C. Potter, David A. Plaisted
Term Rewriting: Some Experimental Results. CADE (1988)
David A. Plaisted
A Goal Directed Theorem Prover. CADE (1988)
David A. Plaisted, Jiarong Hong
A Heuristic Triangulation Algorithm. J. Algorithms 8 (3) (1987)
Bharat Jayaraman, David A. Plaisted
Functional programming with sets. FPCA (1987)
David A. Plaisted
A Logic for Conditional Term Rewriting Systems. CTRS (1987)
David A. Plaisted
Abstraction Using Generalization Functions. CADE (1986)
David A. Plaisted
A Simple Non-Termination Test for the Knuth-Bendix Method. CADE (1986)
David A. Plaisted
A Decision Procedure for Combinations of Propositional Temporal Logic and Other Specialized Theories. J. Autom. Reason. 2 (2) (1986)
Steven Greenbaum, David A. Plaisted
The Illinois Prover: A General Purpose Resolution Theorem Prover. CADE (1986)
David A. Plaisted
The Denotional Semantics of Nondeterministic Recursive Programs using Coherent Relations LICS (1986)
J. Dean Brock, Amos R. Omondi, David A. Plaisted
A Multiprocessor Architecture for Medium-Grain Parallelism. ICDCS (1986)
David A. Plaisted, Steven Greenbaum
A Structure-Preserving Clause Form Translation. J. Symb. Comput. 2 (3) (1986)
David A. Plaisted, J. W. Curry
Extensions to functional programming in Scheme. ISMIS (1986)
David A. Plaisted
An Architecture for fast Data Movement in the FFP Machine. FPCA (1985)
David A. Plaisted
Semantic Confluence Tests and Completion Methods Inf. Control. 65 (2/3) (1985)
David A. Plaisted
Complete Divisibility Problems for Slowly Utilized Oracles. Theor. Comput. Sci. 35 (1985)
Nachum Dershowitz, David A. Plaisted
Logic Programming cum Applicative Programming. SLP (1985)
Leo Bachmair, David A. Plaisted
Termination Orderings for Associative-Commutative Rewriting Systems. J. Symb. Comput. 1 (4) (1985)
Leo Bachmair, David A. Plaisted
Associative Path Orderings. RTA (1985)
Nachum Dershowitz, David A. Plaisted
Conditional rewriting. ACM SIGSOFT Softw. Eng. Notes 10 (4) (1985)
David A. Plaisted
The Undecidability of Self-Embedding for Term Rewriting Systems. Inf. Process. Lett. 20 (2) (1985)
David A. Plaisted
Complete Problems in the First-Order Predicate Calculus. J. Comput. Syst. Sci. 29 (1) (1984)
David A. Plaisted
An Efficient Bug Location Algorithm. ICLP (1984)
David A. Plaisted
Using Examples, Case Analysis, and Dependency Graphs in Theorem Proving. CADE (1984)
David A. Plaisted
Heuristic Matching for Graphs Satisfying the Triangle Inequality. J. Algorithms 5 (2) (1984)
David A. Plaisted
The Occur-Check Problem in Prolog. SLP (1984)
David A. Plaisted
New NP-Hard and NP-Complete Polynomial and Integer Divisibility Problems. Theor. Comput. Sci. 31 (1984)
David A. Plaisted
The Occur-Check Problem in Prolog. New Gener. Comput. 2 (4) (1984)
Nachum Dershowitz, Jieh Hsiang, N. Alan Josephson, David A. Plaisted
Associative-Commutative Rewriting. IJCAI (1983)
David A. Plaisted
A Low Level Language for Obtaining Decision Procedure for Classes of temporal Logics. Logic of Programs (1983)
Kenneth J. Supowit, Edward M. Reingold, David A. Plaisted
The Travelling Salesman Problem and Minimum Matching in the Unit Square. SIAM J. Comput. 12 (1) (1983)
Steven Greenbaum, A. Nagasaka, Paul O'Rorke, David A. Plaisted
Comparison of Natural Deduction and Locking Resolution Implementations. CADE (1982)
David A. Plaisted
A Simplified Problem Reduction Format. Artif. Intell. 18 (2) (1982)
David A. Plaisted
Theorem Proving with Abstraction. Artif. Intell. 16 (1) (1981)

David A. Plaisted.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

David A. Plaisted