David A. Plaisted

116 papers A* 11A 16B 2C 4Journal 57Unranked 22

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