To the Computer Science Department home page
(919) 590-6051 (Voice)
(919) 590-6105 (Fax)
My email address is plaisted at cs.unc.edu
Secretary:Bridgette Cyr
(919) 590-6222 (Voice)
cyr (at) cs.unc.edu (e-mail)
We are investigating methods of combining term-rewriting systems with first-order theorem provers. We developed a way of handling AC symbols using permutations and implemented it. We also studied techniques for applying efficient permutation group algorithms to equational theorem proving.
Mechanical theorem proving. We are investigating methods to automate the process of searching for and checking proofs. This has applications to program verification and to teaching logic and mathematics, since a proof checker can be helpful for instructional purposes. We have developed a sequence of theorem-proving methods, the most recent being clause linking with semantics and ordered semantic hyper-linking. At the same time, we have developed analytical methods for studying the search efficiencies of theorem-proving strategies. As a result, we have developed provers that are among the best in terms of being able to prove a wide variety of non-equality problems with a minimum of human guidance. We have applied these provers to problems involving concept description languages in AI and planning problems, with good results.
We have also investigated rigid E-unification, which is a version of unification relevant for certain theorem proving methods (based on "matings").
Logic programming. We have developed some simple but effective tests that permit the occurrence check in Prolog to be eliminated in most cases, while guaranteeing the same semantics as true unification.
Program verification. We have developed theoretical methods for automatically generating the inductive assertions in program verification. We would like to see to what extent this can be implemented and applied to program verification.
Program generation. We are studying the proofs-as-programs paradigm, in which programs are expressed as proofs in a logical system. This system permits the generation of programs that are correct with respect to their specifications. Our approach combines constructive and classical logic, with classical logic being used for the parts of the proofs that have no computational content. Also, our approach can handle nondeterminism and nonterminating programs.
Maria Paola Bonacina and David A. Plaisted. Constraint manipulation in SGGS. In Notes of the Twenty-Eighth Workshop on Unification (UNIF), Seventh International Joint Conference on Automated Reasoning (IJCAR) and Sixth Federated Logic Conference (FLoC), Vienna, Austria, July 2014. Technical Report 14-06, Research Institute for Symbolic Computation, Johannes Kepler Universitaet, Linz, 47-54, 2014.
Maria Paola Bonacina and David A. Plaisted. Semantically-guided goal-sensitive theorem proving (Abstract). Annual Meeting of the IFIP Working Group in Term Rewriting (WG 1.6), Sixth Federated Logic Conference (FLoC), Vienna, Austria, July 2014.
D. Plaisted, Source-to-Source Translation and Software Engineering, JSEA Special Issue on Software Dependability, Vol. 6 No. 4A, April, 2013.
David Plaisted and Swaha Miller, The Relative Power of Semantics and Unification, in: Programming Logics: Essays in Memory of Harald Ganzinger (Lecture Notes in Computer Science / Theoretical Computer Science and General Issues), Andrei Voronkov and Christoph Weidenbach (Editors), Springer, March 13, 2013.
D. Plaisted, Theorem Proving, in Encyclopedia of Computer Science and Engineering, Benjamin W. Wah, editor, John Wiley and Sons, Hoboken, NJ, January 2009, pp.223-244.
Vladimir Lifschitz, Leora Morgenstern, and David Plaisted, Knowledge Representation and Classical Logic, in Handbook of Knowledge Representation, F. van Harmelen, V. Lifschitz, and B. Porter, eds., 2008, Elsevier, pp. 3-88.
Swaha Miller and David A. Plaisted, The Space Efficiency of OSHL, International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2005), Bernhard Beckert, editor, Koblenz, Germany, September 14-17, 2005.
Swaha Miller and David A. Plaisted, Performance of OSHL on Problems Requiring Definition Expansion, 7th International Workshop on First-Order Theorem Proving, Reinhold Letz, editor, Koblenz, Germany, September 15-17, 2005.
David Plaisted and Swaha Miller, The Relative Power of Semantics and Unification, Workshop on Programming Logics in memory of Harald Ganzinger, Andreas Podelski, Andrei Voronkov and Reinhard Wilhelm, editors, Saarbruecken, Germany, June 3-4, 2005.
David A. Plaisted, Armin Biere, Yunshan Zhu, A satisfiability procedure for quantified Boolean formulae, Discrete Applied Mathematics 130 (2003) 291-328.
David Plaisted, A Hierarchical Situation Calculus , January, 2003, unpublished.
David Plaisted, An Abstract Programming System, November, 2002, unpublished.
Adnan Yahya and David Plaisted, Ordered Semantic Hyper-Tableaux, Journal of Automated Reasoning 29 (1): 17-57, July, 2002.
Nachum Dershowitz and David Plaisted, Rewriting, in Handbook of Automated Reasoning, Volume 1, Alan Robinson and Andrei Voronkov, eds, North-Holland, 2001, pp. 535-610.
J. Avenhaus and D. Plaisted, General algorithms for permutations in equational inference, Journal of Automated Reasoning, Vol. 26, no. 3 (April 2001) 223-268.
David A. Plaisted and Yunshan Zhu, Ordered Semantic Hyper Linking, Journal of Automated Reasoning 25(3):167-217, October 2000.
David A. Plaisted, Special cases and substitutes for rigid E-unification, Applicable Algebra in Engineering, Communication and Computing, Vol 10, No. 2 (2000) 97-152.
David A. Plaisted and Gregory Kucherov, The complexity of some complementation problems, Information Processing Letters 71 (1999) 159-165.
David A. Plaisted and Yunshan Zhu, Replacement Rules with Definition Detection, invited paper, Automated Deduction in Classical and Non-Classical Logics, Lecture Notes in Artificial Intelligence 1761, Ricardo Caferra and Gernot Salzer, eds., 1999, pp. 80-94.
M. Osoria, B. Jayaraman and D. Plaisted, Theory of Partial Order Programming, Science of Computer Programming 34(3):207--238, 1999.
D. Plaisted, Theorem Proving, in Wiley Encyclopedia of Electrical and Electronics Engineering, Volume 21, John G. Webster, editor, 1999, pp. 662 - 682.
M. Paramasivam and David A. Plaisted, Automated Deduction Techniques for Classification in Description Logic Systems, Journal of Automated Reasoning 20(3), June, 1998, pp. 337-364.
David A. Plaisted and Yunshan Zhu, Equational Reasoning using AC constraints, Fifteenth International Joint Conference on Artificial Intelligence (IJCAI-97), Nagoya, Japan, August 23-29,1997.
M. Paramasivam and David A. Plaisted, RRTP, A Replacement Rule Theorem Prover, JAR 18(2) pp. 221-226, 1997.
Heng Chu and David A. Plaisted, CLINS-S: A Semantically Guided First-Order Theorem Prover, JAR 18(2).
David A. Plaisted and Yunshan Zhu, Ordered Semantic Hyper Linking, Proceedings of Fourteenth National Conference on Artificial Intelligence (AAAI97), July 27 - 31, 1997, Providence, Rhode Island.
Plaisted, D. and Yunshan Zhu, Situation Calculus with Aspect, IASTED International Conference on Artificial Intelligence and Soft Computing'97. Banff, Canada, July 27 -- August 1, 1997.
Yunshan Zhu and D. A. Plaisted, FOLPLAN: A Semantically Guided First-Order Planner, 10th International FLAIRS Conference, Daytona Beach, Florida, May 11-14,1997.
Plaisted, D. and Y. Zhu, The Efficiency of Theorem Proving Strategies, Vieweg, 1997, 170 pp, ISBN: 3-528-05574-X. (To order, contact elisabeth.pflanz@bertelsmann.de.)
Plaisted, D. and G. D. Alexander, Propositional Search Efficiency and First-Order Theorem Proving, SATISFIABILITY PROBLEM: THEORY AND APPLICATIONS (DIMACS Workshop March 11-13, 1996), Ding-Zhu Du, Jun Gu, and Panos Pardalos, eds., (AMS, 1997, Providence, RI), pp. 335-350.
Plaisted, D. A. and Sattler-Klein, A. "Proof Lengths for Equational Completion," Information and Computation 125:2 (March, 1996) 154-170.
Special Issue on Term Rewriting Systems, D. A. Plaisted, ed., Fundamenta Informaticae 24:1,2, Sept.-Oct., 1995, 207 pp.
Lee, Shie-Jue and D. A. Plaisted, Controlling the consumption of storage with sliding priority search in a hyper-linking based theorem prover, Computers and Artificial Intelligence 14:6 (1995) 563-578.
Omondi, A. and Plaisted, D. A., "A model for the parallel execution of subset-equational languages," Future Generation Computer Systems 11:3, June, 1995, 295-320.
Paramasivam, M., and Plaisted, D.A., "Automated Deduction Techniques for Subsumption Checking in Concept Languages," Proc. Fourth Golden West International Conference on Intelligent Systems, San Francisco, Calif., 12-14 June 1995.
Plaisted, D. A. "The Search Efficiency of Theorem Proving Strategies," Proc. 12th Conference on Automated Deduction, Nancy, France, 28 June-1 July 1994. Lecture Notes in Artificial Intelligence #814, Springer-Verlag, 1994, 57-71.
Chu, H., and Plaisted, D.A., "Semantically Guided First-Order Theorem Proving Using Hyper-Linking," Proc. 12th Conference on Automated Deduction, Nancy, France, 28 June-1 July 1994. Lecture Notes in Artificial Intelligence #814, Springer-Verlag, 1994, 192-206.
Chadha, R., and Plaisted, D.A., "Correctness of Unification Without Occur Check in Prolog," Journal of Logic Programming, 18(2), Feb. 1994, 99-122.
Lee, Shie-Jue and Plaisted, D. A. "Use of replace rules in theorem proving," Methods of Logic in Computer Science 1 (1994) 217-240.
Lee, S.-J, and Plaisted, D. A., "Problem Solving by Searching for Models With a Theorem Prover," Artificial Intelligence, 69, 1994, 205-233.
Gabbay, D., H. J. Ohlbach, and D. A. Plaisted. "Killer Transformations," Proc. 1993 Workshop on Proof Theory in Modal Logic, Hamburg, Germany, 18-22 Nov. 1993, 1-45.
Chu, H. and Plaisted, D. A., "Rough Resolution: A Refinement of Resolution to Remove Large Literals," Eleventh National Conference on Artificial Intelligence, Washington, DC, July 11 to July 16, 1993.
Plaisted, D. A., "Polynomial Time Termination and Constraint Satisfaction Tests," Fifth International Conference on Rewriting Techniques and Applications, Montreal, Canada, June 16-18, 1993, pp. 405-420.
Gallier, J., P. Narendran, D. Plaisted, S. Raatz, and W. Snyder. "An Algorithm for Finding Canonical Sets of Ground Rewrite Rules in Polynomial Time," Journal of the ACM, 40(1), 1993, 1-16; reprinted from Proc. Ninth Conference on Automated Deduction.
Chadha, R., and D. A. Plaisted. "On the Mechanical Derivation of Loop Invariants," Journal of Symbolic Computation, 15(5-6), 1993, 705-744.
Plaisted, D. A. "Equational Reasoning and Term Rewriting Systems," Handbook of Logic in Artificial Intelligence and Logic Programming, Vol. 1, D. Gabbay and J. Siekmann, eds., New York, N.Y.: Oxford University Press, 1993, 273-364.
To the faculty information page
To the Computer Science Department home page