David Plaisted | Academic Influence

David Plaisted's AcademicInfluence.com Rankings

David Plaisted

Computer Science

#1430

World Rank

#1479

Historical Rank

Database

#7444

World Rank

#7716

Historical Rank

computer-science Degrees

Download Badge

Computer Science

David Plaisted's Degrees

PhD Computer Science Stanford University
Masters Computer Science Stanford University
Bachelors Mathematics University of California, Berkeley

Similar Degrees You Can Earn

Why Is David Plaisted Influential?

(Suggest an Edit or Addition)

According to Wikipedia, David Alan Plaisted is a computer science professor at the University of North Carolina at Chapel Hill. Research interests Plaisted's research interests include term rewriting systems, automated theorem proving, logic programming, and algorithms. His research accomplishments in theorem proving include work on the recursive path ordering, the associative path ordering, abstraction, the simplified and modified problem reduction formats, ground reducibility, nonstandard clause form translations, rigid E-unification, Knuth–Bendix completion, replacement rules in theorem proving, instance-based theorem proving strategies, and semantics in theorem proving.

(See a Problem?)

David Plaisted's Published Works

Number of citations in a given year to any of this author's works

Total number of citations to an author for the works they published in a given year. This highlights publication of the most important work(s) by the author

Published Works

A Structure-Preserving Clause Form Translation (1986) (627)
In handbook of automated reasoning (2001) (305)
Theorem Proving with Abstraction (1981) (180)
Semantic Confluence Tests and Completion Methods (1985) (146)
Completion Without Failure11This research was supported in part by the National Science Foundation under grants DCR 85–13417 and DCR 85–16243. (1989) (124)
Equational reasoning and term rewriting systems (1993) (124)
New NP-hard and NP-complete polynomial and integer divisibility problems (1977) (117)
Termination Orderings for Associative-Commutative Rewriting Systems (1985) (110)
Eliminating duplication with the hyper-linking strategy (1992) (97)
Equational programming (1986) (91)
Logic Programming cum Applicative Programming (1985) (82)
A Heuristic Triangulation Algorithm (1987) (77)
Ordered Semantic Hyper-Linking (1997) (70)
Rewrite, Rewrite, Rewrite, Rewrite, Rewrite, . . (1991) (62)
Associative-Commutative Rewriting (1983) (62)
A satisfiability procedure for quantified Boolean formulae (2003) (60)
Some polynomial and integer divisibility problems are NP-HARD (1976) (60)
Sparse Complex Polynomials and Polynomial Reducibility (1977) (56)
An algorithm for finding canonical sets of ground rewrite rules in polynomial time (1993) (54)
Rigid E-Unification: NP-Completeness and Applications to Equational Matings (1990) (53)
The Travelling Salesman Problem and Minimum Matching in the Unit Square (1983) (53)
Semantically Guided First-Order Theorem Proving using Hyper-Linking (1994) (51)
A Simplified Problem Reduction Format (1982) (50)
Complete Problems in the First-Order Predicate Calculus (1984) (49)
Knowledge Representation and Classical Logic (2008) (48)
PROGRAMMING WITH PARAMETERIZED ABSTRACT OBJECTS IN OBJ. (1983) (47)
Programming with Equations, Subsets, and Relations (1989) (45)
The Search Efficiency of Theorem Proving Strategies (1994) (45)
Heuristics for weighted perfect matching (1980) (44)
Completion without Failure 1 (1989) (41)
Proof Lengths for Equational Completion (1996) (40)
Rigid E-unification is NP-complete (1988) (40)
Polynomial Time Termination and Constraint Satisfaction Tests (1993) (38)
Non-Horn clause logic programming without contrapositives (1988) (37)
Associative Path Orderings (1985) (36)
Abstraction Mappings in Mechanical Theorem Proving (1980) (32)
Functional programming with sets (1987) (31)
Finding Canonical Rewriting Systems Equivalent to a Finite Set of Ground Equations in Polynomial Time (1988) (31)
A relevance restriction strategy for automated deduction (2003) (31)
The Undecidability of Self-Embedding for Term Rewriting Systems (1985) (30)
The Efficiency of Theorem Proving Strategies (1999) (28)
A Simple Non-Termination Test for the Knuth-Bendix Method (1986) (23)
Correctness of Unification Without Occur Check in Prolog (1994) (23)
Theory of Partial-Order Programming (1999) (22)
Heuristic Matching for Graphs Satisfying the Triangle Inequality (1984) (21)
Fast Verification, Testing, and Generation of Large Primes (1979) (21)
Special Cases and Substitutes for Rigid E-Unification (2000) (20)
Infinite Normal Forms (Preliminary Version) (1989) (20)
On the Mechanical Derivation of Loop Invariants (1993) (20)
Semantically-Guided Goal-Sensitive Reasoning: Inference System and Completeness (2017) (19)
Source-to-Source Translation and Software Engineering (2013) (19)
Semantically-Guided Goal-Sensitive Reasoning: Model Representation (2016) (18)
Problem Solving by Searching for Models with a Theorem Prover (1994) (17)
Clin: an automated reasoning system using clause linking (1990) (17)
SGGS Theorem Proving: an Exposition (2014) (17)
An Efficient Bug Location Algorithm (1984) (17)
A Heuristic Algorithm for Small Separators in Arbitrary Graphs (1990) (17)
Model Finding in Semantically Guided Instance-Based Theorem Proving (1994) (16)
A Complete Semantic Back Chaining Proof System (1990) (16)
A decision procedure for combinations of propositional temporal logic and other specialized theories (1986) (14)
Term Rewriting: Some Experimental Results (1988) (13)
A sequent-style model elimination strategy and a positive refinement (1990) (12)
Automated Deduction Techniques for Classification in Description Logic Systems (1998) (12)
Comparison of Natural Deduction and Locking Resolution Implementations (1982) (12)
A Low Level Language for Obtaining Decision Procedure for Classes of temporal Logics (1983) (12)
An NP-complete matching problem (1980) (11)
General Algorithms for Permutations in Equational Inference (2001) (11)
The search efficiency of theorem proving strategies: an analytical comparison (1994) (11)
Abstraction Using Generalization Functions (1986) (11)
Use of replace rules in theorem proving (1994) (10)
An Efficient Relevance Criterion for Mechanical Theorem Proving (1980) (10)
CLIN-S - A Semantically Guided First-Order Theorem Prover (1997) (10)
Conditional Term Rewriting and First-Order Theorem Proving (1992) (10)
Ordered Semantic Hyper Tableaux (2002) (9)
Theorem proving and semantic trees (1976) (9)
History and Prospects for First-Order Automated Deduction (2015) (9)
Flowchart schemata with counters (1972) (8)
Proving Equality Theorems with Hyper-Linking (1992) (8)
The occur-check problem in Prolog (1984) (8)
A Multiprocessor Architecture for Medium-Grain Parallelism (1986) (8)
Constraint manipulation in SGGS (2014) (8)
A Hierarchical Situation Calculus (2003) (8)
Conditional rewriting (1985) (8)
The efficiency of theorem proving strategies - a comparative and asymptotic analysis (1999) (7)
A Logic for Conditional Term Rewriting Systems (1988) (7)
Rough Resolution: A Refinement of Resolution to Remove Large Literals (1993) (6)
New applications of a fast propositional calculus decision procedure (1990) (6)
Complete Divisibility Problems for Slowly Utilized Oracles (1985) (6)
Equational Reasoning using AC Constraints (1997) (6)
Replacement Rules with Definition Detection (1998) (6)
IMPLEMENTATION OF AN IMPROVED RELEVANCE CRITERION. (1984) (6)
Finding Logical Consequences Using Unskolemization (1993) (6)
Using Examples, Case Analysis, and Dependency Graphs in Theorem Proving (1984) (5)
An Architecture for fast Data Movement in the FFP Machine (1985) (5)
RRTP - A Replacement Rule Theorem Prover (1997) (5)
Rewrite, Rewrite, Rewrite (1989) (5)
Model Finding Strategies in Semantically Guided Instance-based Theorem Proving (1993) (5)
The Relative Power of Semantics and Unification (2013) (4)
A Semantic Backward Chaining Proof System (1992) (4)
PROBLEM REPRESENTATION FOR BACK CHAINING AND EQUALITY IN RESOLUTION THEOREM PROVING. (1984) (4)
An Abstract Programming System (2003) (4)
Automated theorem proving. (2014) (4)
Proving First-Order Equality Theorems with Hyper-Linking (1995) (4)
Reasoning with predicate replacement (1991) (4)
Propositional theorem proving by semantic tree trimming for hardware verification (1999) (3)
The Illinois Prover: A General Purpose Resolution Theorem Prover (1986) (3)
Refinements to Depth-First Iterative-Deepening Search in Automatic Theorem Proving (1989) (3)
Semantically-guided goal-sensitive theorem proving (2014) (3)
Propositional search efficiency and first-order theorem proving (1996) (2)
The Denotional Semantics of Nondeterministic Recursive Programs using Coherent Relations (1986) (2)
Instance-based first-order methods using propositional calculus provers (1997) (2)
Situation Calculus with Aspect (1997) (2)
The Application of Multivariate Polynomials to Inference Rules and Partial Tests for Unsatisfiability (1980) (2)
Experimental Results on Subgoal Reordering (1990) (2)
A Game-Based Architecture for Developing Interactive Components in Computational Logic (2000) (1)
The Space Efficiency of OSHL (2005) (1)
A Term-Rewriting Semantics for Imperative Style Programming (2020) (1)
Semantically-guided goal-sensitive theorem proving (Abstract) (2014) (1)
Efficient first-order semantic deduction techniques (1998) (1)
On the distribution of independent formulae of number theory (1980) (1)
An abstract program generation logic (1994) (1)
The Complexity of Some Complementation Problems (1999) (1)
An architecture for functional programming and term rewriting (1986) (1)
The Use of Semantics in Instance-based Proof Procedures ? (1994) (1)
Automated Deduction Techniques for Classification in Concept Languages (1996) (1)
Automatic theorem-proving in problem reduction formats (1989) (1)
Use of unit clauses and clause splitting in automatic deduction (1992) (1)
Semantics of Subset-logic Programming @bullet (2009) (0)
Inference by Clause Linking TR 90-022 May , 1990 (2010) (0)
Situation Calculus by Term Rewriting (2020) (0)
Controlling the Consumption of Storage with Sliding Priority Search in a Hyper-Linking Based Theorem Prover (1995) (0)
An Improved Propositional Approach to First-Order Theorem Proving (2007) (0)
Semantically-Guided Goal-Sensitive Reasoning: Inference System and Completeness (2016) (0)
Oshl-u: a first order theorem prover using propositional techniques and semantics (2005) (0)
Max-planck-institut F Ur Informatik an Abstract Program Generation Logic K I N F O R M a T I K Im Stadtwald D 66123 Saarbr Ucken Germany Authors' Addresses (1994) (0)
On the Mechanica l Der ivat ion of Loop Invariants (2007) (0)
The Journal of Functional and Logic Programming the Journal of Functional and Logic Programming Compile-time Pointer Reversal (1996) (0)
Implementation J \ otes on SPRFN-A Natural Deduction Theorem Prover TR 87-028 September , 1987 (2008) (0)
A decision procedure for quantified boolean formulae (2000) (0)
A Goal Directed Theorem Prover (1988) (0)
Relevance and Abstraction (2021) (0)
Application of EA " J ) lanation-Based Generalization in Theorem Proving * TR 89-015 March 1989 (2009) (0)
Properties and Extensions of Alternating Path Relevance - I (2019) (0)
A model for the parallel execution of subset-equational languages (1995) (0)
Management of the TPTP Problem Set (2021) (0)
Contents to Volume 25 (1991) (0)
A Semantic Variant of the Modified Problem Reduction Format * (2009) (0)
Extensions to functional programming in Scheme (1986) (0)
The First-Order Complexity of First-Order Theorem Proving Strategies (1997) (0)
EasyChair Preprint No 1256 The Aspect Calculus (0)
In the next section we consider functional programming using simplification and rewrit ing, and in the section that follows we consider logic programming using unification and nar (1985) (0)
Contents to Volume 29 (1983) (0)
Search Spaces for Theorem Proving Strategies (2021) (0)
Max-planck-institut F Ur Informatik Ordered Semantic Hyper-linking K I N F O R M a T I K Im Stadtwald D 66123 Saarbr Ucken Germany Authors' Addresses (0)
Max-planck-institut F Ur Informatik Ordered Semantic Hyper-linking K I N F O R M a T I K Im Stadtwald D 66123 Saarbr Ucken Germany Authors' Addresses (0)
The Propositional Complexity of First-Order Theorem Proving Strategies (1997) (0)
Interactive Online Configurator via Boolean Satisfiability Modeling (2021) (0)
The Journal of Functional and Logic Programming the Journal of Functional and Logic Programming a Declarative Debugging Scheme (1997) (0)
ILS: a logic-based expert system representation (1987) (0)
The Aspect Calculus (2019) (0)
Automatic Parallelization of Programs via Software Stream Rewriting (2022) (0)
Max-planck-institut F Ur Informatik Killer Transformations (1994) (0)
Semantically-Guided Goal-Sensitive Reasoning: Model Representation (2015) (0)
CORRECTNESS OF UNIFICATION WITHOUT OCCUR CHECK (2001) (0)

This paper list is powered by the following services:

Other Resources About David Plaisted

en.wikipedia.org

What Schools Are Affiliated With David Plaisted?

David Plaisted is affiliated with the following schools: