Abstract
Logical equivalence between logic programs that are firstorder logic formulas holds between few logic programs, partly because first-order logic does not allow auxiliary programs and data structures to be hidden. As a result of not having such abstractions, logical equivalence will force these auxiliaries to be present in any equivalence program. Higher-order quantification can be use to hide predicates and function symbols. If such higher-order quantification is restricted so that operationally, only hiding is specified, then the cost of such higher-order quantifiers within proof search can be small: one only needs to deal with adding new eigenvariables and clauses involving such eigenvariables. On the other hand, the specification of hiding via quantification can allow for novel and interesting proofs of logical equivalence between programs. This paper will present several example of how reasoning directly on a logic program can benefit significantly if higher-order quantification is used to provide abstractions.
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
This work was supported in part by NSF grants CCR-9912387, CCR-9803971, INT- 9815645, and INT-9815731 and a one month guest professorship at L’Institut de Mathématiques de Luminy, University Aix-Marseille 2 in February 2002.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Jean-Marc Andreoli. Logic programming with focusing proofs in linear logic. Journal of Logic and Computation, 2(3):297–347, 1992.
J. M. Andreoli and R. Pareschi. Linear objects: Logical processes with built-in inheritance. New Generation Computing, 9(3–4):445–473, 1991.
W. W. Bledsoe. A maximal method for set variables in automatic theoremproving. In Machine Intelligence 9, pages 53–100. John Wiley & Sons, 1979.
Iliano Cervesato, Nancy A. Durgin, Patrick D. Lincoln, John C. Mitchell, and Andre Scedrov. A meta-notation for protocol analysis. In R. Gorrieri, editor, Proceedings of the 12th IEEE Computer Security Foundations Workshop—CSFW’99, pages 55–69, Mordano, Italy, 28–30 June 1999. IEEE Computer Society Press.
Iliano Cervesato, Nancy A. Durgin, Patrick D. Lincoln, John C. Mitchell, and Andre Scedrov. Relating strands and multiset rewriting for security protocol analysis. In P. Syverson, editor, 13th IEEE Computer Security Foundations Workshop—CSFW’00, pages 35–51, Cambrige, UK, 3–5 July 2000. IEEE Computer Society Press.
Alonzo Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5:56–68, 1940.
Gilles Dowek. A complete proof synthesis method for the cube of type systems. Journal of Logic and Computation, 3(3):287–315, 1993.
Amy Felty. The calculus of constructions as a framework for proof search with set variable instantiation. Theoretical Computer Science, 232(1–2):187–229, February 2000.
Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50:1–102, 1987.
Joshua Hodas and Dale Miller. Logic programming in a fragment of intuitionistic linear logic. Information and Computation, 110(2):327–365, 1994.
Gérard Huet. A unification algorithm for typed λ-calculus. Theoretical Computer Science, 1:27–57, 1975.
Max Kanovich. Horn programming in linear logic is NP-complete. In Proceedings of the Seventh Annual IEEE Synposium on Logic in Computer Science, pages 200–210. IEEE Computer Society Press, June 1992.
Max Kanovich. The complexity of Horn fragments of linear logic. Annals of Pure and Applied Logic, 69:195–241, 1994.
Dale Miller. An overview of linear logic programming. To appear in a book on linear logic, edited by Thomas Ehrhard, Jean-Yves Girard, Paul Ruet, and Phil Scott. Cambridge University Press.
Dale Miller. Lexical scoping as universal quantification. In Sixth International Logic Programming Conference, pages 268–283, Lisbon, Portugal, June 1989. MIT Press.
Dale Miller. A logical analysis of modules in logic programming. Journal of Logic Programming, 6(1–2):79–108, January 1989.
Dale Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. Journal of Logic and Computation, 1(4):497–536, 1991.
Dale Miller. The π-calculus as a theory in linear logic: Preliminary results. In E. Lamma and P. Mello, editors, Proceedings of the 1992 Workshop on Extensions to Logic Programming, number 660 in LNCS, pages 242–265. Springer-Verlag, 1993.
Dale Miller. Forum: A multiple-conclusion specification language. Theoretical Computer Science, 165(1):201–232, September 1996.
Dale Miller, Gopalan Nadathur, Frank Pfenning, and Andre Scedrov. Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic, 51:125–157, 1991.
Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile processes, Part I. Information and Computation, pages 1–40, September 1992.
Gopalan Nadathur and Dale Miller. Higher-order Horn clauses. Journal of the ACM, 37(4):777–814, October 1990.
Gopalan Nadathur and Dustin J. Mitchell. System description: Teyjus—a compiler and abstract machine based implementation of Lambda Prolog. In H. Ganzinger, editor, Proceedings of the 16th International Conference on Automated Deduction, pages 287–291, Trento, Italy, July 1999. Springer-Verlag LNCS.
Frank Pfenning and Conal Elliott. Higher-order abstract syntax. In Proceedings of the ACM-SIGPLAN Conference on Programming Language Design and Implementation, pages 199–208. ACM Press, June 1988.
Paul Syverson and Iliano Cervesato. The logic of authentication protocols. In R. Focardi and R. Gorrieri, editors, Foundations of Security Analysis and Design, volume LNCS 2171. Springer-Verlag, 2001.
Anne S. Troelstra. Lectures on Linear Logic. CSLI Lecture Notes 29, Center for the Study of Language and Information, Stanford, California, 1992.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Miller, D. (2002). Higher-Order Quantification and Proof Search* . In: Kirchner, H., Ringeissen, C. (eds) Algebraic Methodology and Software Technology. AMAST 2002. Lecture Notes in Computer Science, vol 2422. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45719-4_5
Download citation
DOI: https://doi.org/10.1007/3-540-45719-4_5
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-44144-1
Online ISBN: 978-3-540-45719-0
eBook Packages: Springer Book Archive