David A. Plaisted - researchr alias

researchr

You are not signed in
Sign in
Sign up

Viewing Publication 1 - 100 from 110

2022

Automatic Parallelization of Programs via Software Stream RewritingTao Tao, David A. Plaisted. ipps 2022: 541-551 [doi]

2021

Relevance and AbstractionDavid A. Plaisted. arcade 2021: 1-4 [doi]

Search Spaces for Theorem Proving StrategiesDavid A. Plaisted. arcade 2021: 1-3 [doi]

Management of the TPTP Problem SetGeoff Sutcliffe, David A. Plaisted. arcade 2021: 1 [doi]

Interactive Online Configurator via Boolean Satisfiability ModelingTao Tao, David A. Plaisted. iait 2021: [doi]

2019

The Aspect CalculusDavid A. Plaisted. cade 2019: 406-424 [doi]

2017

Semantically-Guided Goal-Sensitive Reasoning: Inference System and CompletenessMaria Paola Bonacina, David A. Plaisted. JAR, 59(2):165-218, 2017. [doi]

2016

Semantically-Guided Goal-Sensitive Reasoning: Model RepresentationMaria Paola Bonacina, David A. Plaisted. JAR, 56(2):113-141, 2016. [doi]

2015

History and Prospects for First-Order Automated DeductionDavid A. Plaisted. cade 2015: 3-28 [doi]

2014

SGGS Theorem Proving: an ExpositionMaria Paola Bonacina, David A. Plaisted. cade 2015: 25-38 [doi]

Constraint Manipulation in SGGSMaria Paola Bonacina, David A. Plaisted. UNIF 2014: 47-54 [doi]

2013

The Relative Power of Semantics and UnificationDavid A. Plaisted, Swaha Miller. BIRTHDAY 2013: 317-344 [doi]

2005

The Space Efficiency of OSHLSwaha Miller, David A. Plaisted. tableaux 2005: 217-230 [doi]

2003

A relevance restriction strategy for automated deductionDavid A. Plaisted, Adnan H. Yahya. ai, 144(1-2):59-93, 2003. [doi]

A satisfiability procedure for quantified Boolean formulaeDavid A. Plaisted, Armin Biere, Yunshan Zhu. DAM, 130(2):291-328, 2003. [doi]

2002

Ordered Semantic Hyper TableauxAdnan H. Yahya, David A. Plaisted. JAR, 29(1):17-57, 2002.

2001

General Algorithms for Permutations in Equational InferenceJürgen Avenhaus, David A. Plaisted. JAR, 26(3):223-268, 2001.

RewritingNachum Dershowitz, David A. Plaisted. In John Alan Robinson, Andrei Voronkov, editors, Handbook of Automated Reasoning (in 2 volumes). pages 535-610, Elsevier and MIT Press, 2001.

2000

Ordered Semantic Hyper-LinkingDavid A. Plaisted, Yunshan Zhu. JAR, 25(3):167-217, 2000.

Special Cases and Substitutes for Rigid E-UnificationDavid A. Plaisted. aaecc, 10(2):97-152, 2000. [doi]

1999

Theory of Partial-Order ProgrammingMauricio Osorio, Bharat Jayaraman, David A. Plaisted. SCP, 34(3):207-238, 1999.

The Complexity of Some Complementation ProblemsDavid A. Plaisted, Gregory Kucherov. ipl, 71(3-4):159-165, 1999. [doi]

1998

Automated Deduction Techniques for Classification in Description Logic SystemsM. Paramasivam, David A. Plaisted. JAR, 20(3):337-364, 1998.

Replacement Rules with Definition DetectionDavid A. Plaisted, Yunshan Zhu. ftp 2000: 80-94 [doi]

1997

CLIN-S - A Semantically Guided First-Order Theorem ProverHeng Chu, David A. Plaisted. JAR, 18(2):183-188, 1997.

RRTP - A Replacement Rule Theorem ProverM. Paramasivam, David A. Plaisted. JAR, 18(2):221-226, 1997.

The efficiency of theorem proving strategies - a comparative and asymptotic analysisDavid A. Plaisted, Yunshan Zhu. Computational intelligence, Vieweg, 1997.

Equational Reasoning using AC ConstraintsDavid A. Plaisted, Yunshan Zhu. IJCAI 1997: 108-113

Ordered Semantic Hyper LinkingDavid A. Plaisted, Yunshan Zhu. AAAI 1997: 472-477

1996

Propositional search efficiency and first-order theorem provingDavid A. Plaisted, Geoffrey D. Alexander. dimacs 1997: 335-350

Proof Lengths for Equational CompletionDavid A. Plaisted, Andrea Sattler-Klein. iandc, 125(2):154-170, 1996.

1995

Controlling the Consumption of Storage with Sliding Priority Search in a Hyper-Linking Based Theorem ProverShie-Jue Lee, David A. Plaisted. cai, 14(6):563-578, 1995.

A model for the parallel execution of subset-equational languagesAmos R. Omondi, David A. Plaisted. fgcs, 11(3):295-320, 1995. [doi]

1994

1993

1992

1991

Rewrite, Rewrite, Rewrite, Rewrite, Rewrite, . . Nachum Dershowitz, Stéphane Kaplan, David A. Plaisted. TCS, 83(1):71-96, 1991.

Term Rewriting: Some Experimental ResultsDavid A. Plaisted, Richard C. Potter. JSC, 11(1/2):149-180, 1991.

1990

Rigid E-Unification: NP-Completeness and Applications to Equational MatingsJean H. Gallier, Paliath Narendran, David A. Plaisted, Wayne Snyder. iandc, 87(1/2):129-195, July/August 1990.

A Complete Semantic Back Chaining Proof SystemXumin Nie, David A. Plaisted. cade 1990: 16-27

Experimental Results on Subgoal ReorderingXumin Nie, David A. Plaisted. TC, 39(6):845-848, 1990.

A Sequent-Style Model Elimination Strategy and a Positive RefinementDavid A. Plaisted. JAR, 6(4):389-402, 1990.

A Heuristic Algorithm for Small Separators in Arbitrary GraphsDavid A. Plaisted. SICOMP, 19(2):267-280, 1990.

1989

Infinite Normal Forms (Preliminary Version)Nachum Dershowitz, Stéphane Kaplan, David A. Plaisted. icalp 1989: 249-262

Programming with Equations, Subsets, and RelationsBharat Jayaraman, David A. Plaisted. SLP 1989: 1051-1068

Refinements to Depth-First Iterative-Deepening Search in Automatic Theorem ProvingXumin Nie, David A. Plaisted. ai, 41(2):223-235, 1989.

1988

1987

Functional programming with setsBharat Jayaraman, David A. Plaisted. fpca 1987: 194-211

A Logic for Conditional Term Rewriting SystemsDavid A. Plaisted. ctrs 1988: 212-227

A Heuristic Triangulation AlgorithmDavid A. Plaisted, Jiarong Hong. jal, 8(3):405-437, 1987.

1986

A Multiprocessor Architecture for Medium-Grain ParallelismJ. Dean Brock, Amos Omondi, David A. Plaisted. icdcs 1986: 167-174

The Illinois Prover: A General Purpose Resolution Theorem ProverSteven Greenbaum, David A. Plaisted. cade 1986: 685-687

A Simple Non-Termination Test for the Knuth-Bendix MethodDavid A. Plaisted. cade 1986: 79-88

Extensions to functional programming in SchemeDavid A. Plaisted, J. W. Curry. ismis 1986: 230-246 [doi]

The Denotional Semantics of Nondeterministic Recursive Programs using Coherent RelationsDavid A. Plaisted. lics 1986: 163-174

Abstraction Using Generalization FunctionsDavid A. Plaisted. cade 1986: 365-376

A Decision Procedure for Combinations of Propositional Temporal Logic and Other Specialized TheoriesDavid A. Plaisted. JAR, 2(2):171-190, 1986.

A Structure-Preserving Clause Form TranslationDavid A. Plaisted, Steven Greenbaum. JSC, 2(3):293-304, 1986.

1985

Associative Path OrderingsLeo Bachmair, David A. Plaisted. RTA 1985: 241-254

Termination Orderings for Associative-Commutative Rewriting SystemsLeo Bachmair, David A. Plaisted. JSC, 1(4):329-349, 1985.

Logic Programming cum Applicative ProgrammingNachum Dershowitz, David A. Plaisted. SLP 1985: 54-66

Conditional rewritingNachum Dershowitz, David A. Plaisted. sigsoft, 10(4):55-59, 1985. [doi]

An Architecture for fast Data Movement in the FFP MachineDavid A. Plaisted. fpca 1985: 147-163

The Undecidability of Self-Embedding for Term Rewriting SystemsDavid A. Plaisted. ipl, 20(2):61-64, 1985.

Complete Divisibility Problems for Slowly Utilized OraclesDavid A. Plaisted. TCS, 35:245-260, 1985.

Semantic Confluence Tests and Completion MethodsDavid A. Plaisted. iandc, 65(2/3):182-215, May/June 1985.

1984

1983

Associative-Commutative RewritingNachum Dershowitz, Jieh Hsiang, N. Alan Josephson, David A. Plaisted. IJCAI 1983: 940-944

A Low Level Language for Obtaining Decision Procedure for Classes of temporal LogicsDavid A. Plaisted. lop 1984: 403-420

The Traveling Salesman Problem and Minimum Matching in the Unit SquareKenneth J. Supowit, Edward M. Reingold, David A. Plaisted. SICOMP, 12(1):144-156, 1983.

1982

Comparison of Natural Deduction and Locking Resolution ImplementationsSteven Greenbaum, A. Nagasaka, Paul O Rorke, David A. Plaisted. cade 1982: 159-171

A Simplified Problem Reduction FormatDavid A. Plaisted. ai, 18(2):227-261, 1982.

1981

Theorem Proving with AbstractionDavid A. Plaisted. ai, 16(1):47-108, 1981.

1980

An Efficient Relevance Criterion for Mechanical Theorem ProvingDavid A. Plaisted. AAAI 1980: 79-83

Abstraction Mappings in Mechanical Theorem ProvingDavid A. Plaisted. cade 1980: 264-280

Heuristics for Weighted Perfect MatchingKenneth J. Supowit, David A. Plaisted, Edward M. Reingold. stoc 1980: 398-419

Sign in or sign up to see more results.

runs on WebDSL