Hostname: page-component-cd9895bd7-7cvxr Total loading time: 0 Render date: 2024-12-23T10:17:48.650Z Has data issue: false hasContentIssue false
  • English
  • Français

A Survey of the Proof-Theoretic Foundations of Logic Programming

Published online by Cambridge University Press:  18 November 2021

DALE MILLER Open the ORCID record for DALE MILLER [Opens in a new window]
DALE MILLER*
Affiliation:
Inria-Saclay & LIX, Ecole Polytechnique, Palaiseau, France (e-mail: [email protected])
Get access Rights & Permissions [Opens in a new window]

Abstract

Several formal systems, such as resolution and minimal model semantics, provide a framework for logic programming. In this article, we will survey the use of structural proof theory as an alternative foundation. Researchers have been using this foundation for the past 35 years to elevate logic programming from its roots in first-order classical logic into higher-order versions of intuitionistic and linear logic. These more expressive logic programming languages allow for capturing stateful computations and rich forms of abstractions, including higher-order programming, modularity, and abstract data types. Term-level bindings are another kind of abstraction, and these are given an elegant and direct treatment within both proof theory and these extended logic programming languages. Logic programming has also inspired new results in proof theory, such as those involving polarity and focused proofs. These recent results provide a high-level means for presenting the differences between forward-chaining and backward-chaining style inferences. Anchoring logic programming in proof theory has also helped identify its connections and differences with functional programming, deductive databases, and model checking.

Type
Original Article
Information
Theory and Practice of Logic Programming , Volume 22 , Issue 6 , November 2022 , pp. 859 - 904
Check for updates
Copyright
© The Author(s), 2021. Published by Cambridge University Press

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Abrusci, V. M. and Ruet, P. 1999. Non-commutative logic I: The multiplicative fragment. Ann. Pure Appl. Log. 101, 1, 29–64.CrossRefGoogle Scholar
Aho, A. V., Lam, M. S., Sethi, R. and Ullman, J. D. 2007. Compilers: Principles, Techniques, and Tools, Second ed. Pearson, Addison Wesley.Google Scholar
Aït-Kaci, H. 1991. Warren’s Abstract Machine: A Tutorial Reconstruction . Logic Programming Research Reports and Notes. MIT Press, Cambridge, MA.Google Scholar
Andreoli, J.-M. 1990. Proposal for a synthesis of logic and object-oriented programming paradigms. Ph.D. thesis, University of Paris VI.Google Scholar
Andreoli, J.-M. 1992. Logic programming with focusing proofs in linear logic. J. Log. Comput. 2, 3, 297–347.CrossRefGoogle Scholar
Andreoli, J. M. and Pareschi, R. 1991. Linear objects: Logical processes with built-in inheritance. New Generation Computing 9, 3–4, 445–473.CrossRefGoogle Scholar
Andrews, J. 1997. A logical semantics for depth-first Prolog with ground negation. Theor. Comput. Sci. 184, 1–2, 105–143.CrossRefGoogle Scholar
Andrews, P. B. 1971. Resolution in type theory. J. Symb. Log. 36, 414–432.CrossRefGoogle Scholar
Andrews, P. B. 1974. Provability in elementary type theory. Zeitschrift fur Mathematische Logic und Grundlagen der Mathematik 20, 411–418.CrossRefGoogle Scholar
Andrews, P. B., Cohen, E. L., Miller, D. and Pfenning, F. 1984. Automating higher order logic. In Automated Theorem Proving: After 25 Years. American Mathematical Society, Providence, RI, 169–192.Google Scholar
Appel, A. W. and Felty, A. P. 1999. Lightweight lemmas in Lambda Prolog. In 16th International Conference on Logic Programming. MIT Press, 411–425.Google Scholar
Apt, K. R. and Bol, R. 1994. Logic programming and negation: A survey. J. Log. Program. 19-20, 9–71.Google Scholar
Apt, K. R. and Doets, K. 1994. A new definition of SLDNF-resolution. The J. Log. Program. 18, 2 (Feb.), 177–190.CrossRefGoogle Scholar
Apt, K. R. and van Emden, M. H. 1982. Contributions to the theory of logic programming. J. ACM 29, 3, 841–862.CrossRefGoogle Scholar
Baelde, D., Chaudhuri, K., Gacek, A., Miller, D., Nadathur, G., Tiu, A. and Wang, Y. 2014. Abella: A system for reasoning about relational specifications. J. Formal. Reason. 7, 2, 1–89.Google Scholar
Banâtre, J.-P. and Métayer, D. L. 1996. Gamma and the chemical reaction model: ten years after. In Coordination programming: Mechanisms, models and semantics. World Scientific Publishing, IC Press, 3–41.Google Scholar
Barendregt, H. 1984. The Lambda Calculus: Its Syntax and Semantics. Vol. 103. Studies in Logic and the Foundations of Mathematics, Elsevier, New York.Google Scholar
Barendregt, H., Dekkers, W. and Statman, R. 2013. Lambda Calculus with Types. Perspectives in Logic, Cambridge University Press.CrossRefGoogle Scholar
Basold, H., Komendantskaya, E. and Li, Y. 2019. Coinduction in uniform: Foundations for corecursive proof search with Horn clauses. In 28th European Symposium on Programming, ESOP 2019, L. Caires, Ed. LNCS, vol. 11423. Springer, 783–813.Google Scholar
Beckert, B. and Posegga, J. 1995. leanTAP: Lean tableau-based deduction. J. Autom. Reason. 15, 3 (Dec.), 339–358.Google Scholar
Bezem, M. 2001. An improved extensionality criterion for higher-order logic programs. In CSL: 15th Workshop on Computer Science Logic, L. Fribourg, Ed. LNCS, vol. 2142. Springer-Verlag, 203–216.Google Scholar
Blanco, R., Chihani, Z. and Miller, D. 2017. Translating between implicit and explicit versions of proof. In 26th International Conference on Automated Deduction (CADE), L. de Moura, Ed. LNCS, vol. 10395. Springer, 255–273.Google Scholar
Börger, E. and Rosenzweig, D. 1995a. A mathematical definition of full Prolog. Sci. Comput. Program. 24, 3, 249–286.CrossRefGoogle Scholar
Börger, E. and Rosenzweig, D. 1995b. The WAM – Definition and compiler correctness. In Logic Programming: Formal Methods and Practical Applications, Studies in Computer Science and Artificial Intelligence, Beierle, C. and Plümer, L., Eds. Elsevier Science B.V./North-Holland, 20–90.Google Scholar
Borras, P., Clément, D., Despeyroux, T., Incerpi, J., Kahn, G., Lang, B. and Pascual, V. 1988. Centaur: the system. In Third Annual Symposium on Software Development Environments (SDE3). ACM, Boston, 14–24.Google Scholar
Bowen, K. A. 1982. Programming with full first-order logic. In Machine Intelligence 10, Hayes, Michie, and Pao, Eds. Horwood, Ellis and Wiley, John, 421–440.Google Scholar
Brewka, G., Eiter, T. and Truszczynski, M. 2011. Answer set programming at a glance. Commun. ACM 54, 12, 92–103.CrossRefGoogle Scholar
Brock-Nannestad, T., Guenot, N. and Gustafsson, D. 2015. Computation in focused intuitionistic logic. In Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming (PPDP), Falaschi, M. and Albert, E., Eds. ACM, 43–54.Google Scholar
De Bruijn, N. G. 1972. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with an application to the Church-Rosser theorem. Indagationes Mathematicae 34, 5, 381–392.CrossRefGoogle Scholar
Bruscoli, P. and Guglielmi, A. 2006. On structuring proof search for first order linear logic. Theor. Comput. Sci. 360, 1–3, 42–76.CrossRefGoogle Scholar
Bugliesi, M., Lamma, E. and Mello, P. 1994. Modularity in logic programming. J. Log. Program. 19/20, 443–502.CrossRefGoogle Scholar
Buss, S. R. 1998. An Introduction to Proof Theory. In Handbook of Proof Theory, S. R. Buss, Ed. Elsevier Science Publishers, Amsterdam, 1–78.Google Scholar
Cellucci, C. 1987. Using full first order logic as a programming language. In Proceedings of the conference on ‘Logic and Computer Science: New Trends and Applications’. Rendiconti del Seminario Matematico Universitae Politecnico di Torino. Fascicolo Speciale 1987, 115–152.Google Scholar
Cervesato, I. 1998. Proof-theoretic foundation of compilation in logic programming languages. In Proceedings of the 1998 Joint International Conference and Symposium on Logic Programming, J. Jaffar, Ed., 115–129.Google Scholar
Cervesato, I., Hodas, J. S. and Pfenning, F. 2000. Efficient resource management for linear logic proof search. Theor. Comput. Sci. 232, 1–2, 133–163.CrossRefGoogle Scholar
Cervesato, I. and Pfenning, F. 1996. A linear logic framework. In 11th Symp. on Logic in Computer Science. IEEE Computer Society Press, New Brunswick, New Jersey, 264–275.Google Scholar
Chaudhuri, K. 2006. The focused inverse method for linear logic. Ph.D. thesis, Carnegie Mellon University. Technical report CMU-CS-06-162.Google Scholar
Chaudhuri, K. 2010a. Classical and intuitionistic subexponential logics are equally expressive. In CSL 2010: Computer Science Logic, Dawar, A. and Veith, H., Eds. LNCS, vol. 6247. Springer, Brno, Czech Republic, 185–199.Google Scholar
Chaudhuri, K. 2010b. Magically constraining the inverse method using dynamic polarity assignment. In Proceedings of 17th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), Fermüller, C. and Voronkov, A., Eds. LNCS, vol. 6397. Springer, Yogyakarta, Indonesia, 202–216.Google Scholar
Chaudhuri, K., Pfenning, F. and Price, G. 2008. A logical characterization of forward and backward chaining in the inverse method. J. Autom. Reason. 40, 2–3 (Mar.), 133–177.CrossRefGoogle Scholar
Chaudhuri, K. and Reis, G. 2015. An adequate compositional encoding of bigraph structure in linear logic with subexponentials. In Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), Davis, M., Fehnker, A., McIver, A., and Voronkov, A., Eds. LNCS, vol. 9450. Springer, 146–161.Google Scholar
Chen, W., Kifer, M. and Warren, D. S. 1993. HILOG: a foundation for higher-order logic programming. J. Log. Program. 15, 3, 187–230.CrossRefGoogle Scholar
Cheney, J. and Urban, C. 2004. Alpha-Prolog: A logic programming language with names, binding, and alpha-equivalence. In Logic Programming, 20th International Conference, Demoen, B. and Lifschitz, V., Eds. LNCS, vol. 3132. Springer, 269–283.Google Scholar
Chihani, Z., Miller, D. and Renaud, F. 2017. A semantic framework for proof evidence. J. Autom. Reason. 59, 3, 287–330.CrossRefGoogle Scholar
Church, A. 1940. A formulation of the simple theory of types. J. Symb. Log. 5, 56–68.CrossRefGoogle Scholar
Clark, K. L. 1978. Negation as failure. In Logic and Data Bases, Gallaire, J. and Minker, J., Eds. Plenum Press, New York, 293–322.Google Scholar
Clément, D., Despeyroux, J., Despeyroux, T., Hascoët, L. and Kahn, G. 1985. Natural semantics on the computer. Research Report 416, INRIA, Rocquencourt, France. June.Google Scholar
Clocksin, W. F. and Mellish, C. S. 1994. Programming in Prolog, Fourth ed. Springer.CrossRefGoogle Scholar
Colmerauer, A. and Roussel, P. 1993. The birth of Prolog. SIGPLAN Notices 28, 3 (Mar.), 37–52.CrossRefGoogle Scholar
Curien, P. and Munch-Maccagnoni, G. 2010. The duality of computation under focus. In Theoretical Computer Science - 6th IFIP TC 1/WG 2.2 International Conference, Calude, C. S. and Sassone, V., Eds. IFIP Advances in Information and Communication Technology, vol. 323. Springer, 165–181.Google Scholar
Curry, H. B. 1934. Functionality in combinatory logic. Proc. Nat. Acad. Sci. 20, 11, 584–590.Google Scholar
Danos, V., Joinet, J.-B., and Schellinx, H. 1993. The structure of exponentials: Uncovering the dynamics of linear logic proofs. In Kurt Gödel Colloquium, Gottlob, G., Leitsch, A., and Mundici, D., Eds. LNCS, vol. 713. Springer, 159–171.Google Scholar
Danos, V., Joinet, J.-B., and Schellinx, H. 1995. LKT and LKQ: sequent calculi for second order logic based upon dual linear decompositions of classical implication. In Advances in Linear Logic, Girard, J.-Y., Lafont, Y., and Regnier, L., Eds. Number 222 in London Mathematical Society Lecture Note Series. Cambridge University Press, 211–224.Google Scholar
Despeyroux, J. 1986. Proof of translation in natural semantics. In 1st Symposium on Logic in Computer Science (LICS). IEEE, Cambridge, Mass, 193–205.Google Scholar
Despeyroux, J., Felty, A. and Hirschowitz, A. 1995. Higher-order abstract syntax in Coq. In Second International Conference on Typed Lambda Calculi and Applications. Springer, 124–138.Google Scholar
Despeyroux, J., Olarte, C. and Pimentel, E. 2016. Hybrid and subexponential linear logics technical report. In Proceedings of LSFA. ENTCS, vol. 332. Elsevier.CrossRefGoogle Scholar
Despeyroux, T. 1984. Executable specification of static semantics. In Semantics of Data Types. LNCS, vol. 173. Springer.CrossRefGoogle Scholar
Despeyroux, T. 1988. TYPOL: A formalism to implement natural semantics. Research Report 94, INRIA, Rocquencourt, France. Mar.Google Scholar
Di Cosmo, R. and Miller, D. 2019. Linear Logic. The Stanford Encyclopedia of Philosophy (Summer 2019 Edition), Edward N. Zalta (ed.). https://plato.stanford.edu/archives/sum2019/entries/logic-linear/.Google Scholar
Donzeau-Gouge, V., Huet, G. and Kahn, G. 1984. Programming environments based on structured editors: the MENTOR experience. In Interactive Programming Environments, Barstow, D. R., Shrobe, H. E., and Sandewall, E., Eds. McGraw-Hill.Google Scholar
Dowling, W. F. and Gallier, J. H. 1984. Linear-time algorithms for testing the satisfiability of propositional Horn formulae. J. Log. Program. 3, 267–284.Google Scholar
Dunchev, C., Guidi, F., Coen, C. S. and Tassi, E. 2015. ELPI: fast, embeddable, λProlog interpreter. In Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20, Davis, M., Fehnker, A., McIver, A., and Voronkov, A., Eds. LNCS, vol. 9450. Springer, 460–468.Google Scholar
Dyckhoff, R. and Lengrand, S. 2006. LJQ: A strongly focused calculus for intuitionistic logic. In Computability in Europe 2006, A. Beckmann and et al., Eds. LNCS, vol. 3988. Springer, 173–185.Google Scholar
Earley, J. 1970. An efficient context-free parsing algorithm. Communications of the ACM 13, 2, 94–102.CrossRefGoogle Scholar
Elliott, C. 1989. Higher-order unification with dependent types. In Rewriting Techniques and Applications. LNCS, vol. 355. Springer, 121–136.Google Scholar
van Emden, M. H. and Kowalski, R. A. 1976. The semantics of predicate logic as a programming language. J. ACM 23, 4, 733–742.CrossRefGoogle Scholar
Espríto Santo, J. E. 2016. The polarized λ-calculus. In 11th Workshop on Logical and Semantic Frameworks with Applications, LSFA 2016, Nigam, V. and Florido, M., Eds. Electronic Notes in Theoretical Computer Science, vol. 332. Elsevier, 149–168.Google Scholar
Fages, F., Ruet, P. and Soliman, S. 1998. Phase semantics and verification of concurrent constraint programs. In 13th Symposium on Logic in Computer Science, V. Pratt, Ed. IEEE.Google Scholar
Fages, F., Ruet, P. and Soliman, S. 2001. Linear concurrent constraint programming: Operational and phase semantics. Information and Computation 165, 1, 14–41.CrossRefGoogle Scholar
Felty, A. 1989. Specifying and implementing theorem provers in a higher-order logic programming language. Ph.D. thesis, University of Pennsylvania.Google Scholar
Felty, A. 1993. Implementing tactics and tacticals in a higher-order logic programming language. J. Autom. Reason. 11, 1, 43–81.CrossRefGoogle Scholar
Felty, A. and Miller, A. 1990. Encoding a Dependent-Type λ-Calculus in a Logic Programming Language. In 10th Conference on Automated Deduction (CADE), M. E. Stickel, Ed. LNAI, vol. 449. Springer, 221–235.Google Scholar
Friedman, D. P., Byrd, W. E., Kiselyov, O. and Hemann, J. 2018. The Reasoned Schemer, Second Edition. The MIT Press.Google Scholar
Gabbay, D. M. 1985. N-Prolog: An extension of Prolog with hypothetical implication II – logical foundations, and negation as failure. J. Log. Program. 2, 4, 251–283.CrossRefGoogle Scholar
Gabbay, D. M. and Reyle, U. 1984. N-Prolog: An extension of Prolog with hypothetical implications. I. J. Log. Program. 1, 319–355.Google Scholar
Gacek, A., Miller, D. and Nadathur, G. 2011. Nominal abstraction. Information and Computation 209, 1, 48–73.CrossRefGoogle Scholar
Gacek, A., Miller, D. and Nadathur, G. 2012. A two-level logic approach to reasoning about computations. J. Autom. Reason. 49, 2, 241–273.CrossRefGoogle Scholar
Gallier, J. H. 1986. Logic for Computer Science: Foundations of Automatic Theorem Proving. Harper & Row, 1986.Google Scholar
Ganzinger, H. and McAllester, D. 2002. Logical algorithms. In Proceedings of International Conference on Logic Programming (ICLP) 2002. LNCS, vol. 2401. Springer, 209–223.Google Scholar
Ganzinger, H. and McAllester, D. A. 2001. A new meta-complexity theorem for bottom-up logic programs. In First International Joint Conference on Automated Reasoning (IJCAR), Goré, R., Leitsch, A., and Nipkow, T., Eds. LNCS, vol. 2083. Springer, 514–528.Google Scholar
Gelfond, M. and Lifschitz, V. 1988. The stable model semantics for logic programming. In Proceedings of the Fifth International Conference on Logic Programming, Kowalski, R. A. and Bowen, K., Eds. The MIT Press, Cambridge, Massachusetts, 1070–1080.Google Scholar
Gentzen, G. 1935. Investigations into logical deduction. In The Collected Papers of Gerhard Gentzen, M. E. Szabo, Ed. North-Holland, Amsterdam, 68–131. Translation of articles that appeared in 1934-35. Collected papers appeared in 1969.Google Scholar
Girard, J.-Y. 1971. Une extension de l’interpretation de Gödel à l’analyse, et son application à l’élimination des coupures dans l’analyse et la théorie des types. In 2nd Scandinavian Logic Symposium, J. E. Fenstad, Ed. North-Holland, Amsterdam, 63–92.Google Scholar
Girard, J.-Y. 1987. Linear logic. Theor. Comput. Sci. 50, 1, 1–102.Google Scholar
Girard, J.-Y., Taylor, P. and Lafont, Y. 1989. Proofs and Types. Cambridge University Press, 1989.Google Scholar
Girard, J.-Y. 1991. A new constructive logic: Classical logic. Math. Struct. Comp. Sci. 1, 255–296.CrossRefGoogle Scholar
Girard, J.-Y. 1992. A fixpoint theorem in linear logic. An email posting to the mailing list .Google Scholar
Gödel, K. 1930. Die vollständigkeit der axiome des logischen funktionenkalküls. Monatshefte für Mathematik 37, 1, 349–360.CrossRefGoogle Scholar
Gordon, M. 2000. From LCF to HOL: A short history. In Proof, Language, and Interaction: Essays in Honour of Robin Milner, Plotkin, G. D., Stirling, C., and Tofte, M., Eds. MIT Press, 169–186.Google Scholar
Gordon, M. J., Milner, A. J. and Wadsworth, C. P. 1979. Edinburgh LCF: A Mechanised Logic of Computation . LNCS, vol. 78. Springer.Google Scholar
Guglielmi, A. 2007. A system of interaction and structure. ACM Trans. Comput. Logic 8, 1 (Jan.), 1–64.Google Scholar
Guidi, F., Coen, C. S. and Tassi, E. 2019. Implementing type theory in higher order constraint logic programming. Mathematical Structures in Computer Science 29, 8, 1125–1150.CrossRefGoogle Scholar
Gunter, C. A. and Gehlot, V. 1989. Nets as tensor theories. Tech. Rep. MS-CIS-89-68, University of Pennsylvania, Computer and Information Science Department.Google Scholar
Hagiya, M. and Sakurai, T. 1984. Foundation of logic programming based on inductive definition. New Generation Computing 2, 1, 59–77.CrossRefGoogle Scholar
Hallnäs, L. and Schroeder-Heister, P. 1990. A proof-theoretic approach to logic programming. I. Clauses as rules. J. Log. Comput. 1, 2, 261–283.CrossRefGoogle Scholar
Hallnäs, L. and Schroeder-Heister, P. 1991. A proof-theoretic approach to logic programming. II. Programs as definitions. J. Log. Comput. 1, 5, 635–660.CrossRefGoogle Scholar
Hannan, J. 1993. Extended natural semantics. J. Funct. Program. 3, 2, 123–152.CrossRefGoogle Scholar
Hannan, J. and Miller, D. 1992. From operational semantics to abstract machines. Mathematical Structures in Computer Science 2, 4, 415–459.CrossRefGoogle Scholar
Hannan, J. and Pfenning, F. 1992. Compiler verification in LF. In 7th Symposium on Logic in Computer Science. IEEE Computer Society Press, Santa Cruz, California.Google Scholar
Hannan, J. J. 1990. Investigating a proof-theoretic meta-language for functional programs. Ph.D. thesis, University of Pennsylvania.Google Scholar
Haridi, S. and Sahlin, D. 1983. Evaluation of logic programs based on natural deduction (draft). In Logic Programming Workshop, Pereira, L. M., Porto, A., Monteiro, L., and Figueiras, M., Eds. Núcleo de Intelligência Artificial, Universidade Nova De Lisboa, Portugal, 560–574.Google Scholar
Harland, J. 1997. On goal-directed provability in classical logic. Comput. Lang 23, 2-4, 161–178.CrossRefGoogle Scholar
Harland, J., Pym, D. and Winikoff, M. 1996. Programming in Lygon: An overview. In Proceedings of the Fifth International Conference on Algebraic Methodology and Software Technology, Eds. Wirsing, M. and Nivat, M.. LNCS, vol. 1101. Springer, 391–405.Google Scholar
Harper, R., Honsell, F. and Plotkin, G. 1993. A framework for defining logics. J. ACM 40, 1, 143–184.CrossRefGoogle Scholar
Harrop, R. 1960. Concerning formulas of the types $A\rightarrow B\lor C,\ A\rightarrow (Ex)B(x)$ in intuitionistic formal systems. J. Symb. Logic 25, 27–32.CrossRefGoogle Scholar
Heath, Q. and Miller, D. 2019. A proof theory for model checking. J. Autom. Reason. 63, 4, 857–885.CrossRefGoogle Scholar
Henkin, L. 1949. The completeness of the first-order functional calculus. J. Symb. Logic 14, 3, 159–166.CrossRefGoogle Scholar
Herbelin, H. 1995. Séquents qu’on calcule: de l’interprétation du calcul des séquents comme calcul de lambda-termes et comme calcul de stratégies gagnantes. Ph.D. thesis, Université Paris 7.Google Scholar
Hodas, J. and Miller, D. 1991. Logic programming in a fragment of intuitionistic linear logic: Extended abstract. In 6th Symp. on Logic in Computer Science, G. Kahn, Ed. IEEE, Amsterdam, 32–42.Google Scholar
Hodas, J. and Miller, D. 1994. Logic programming in a fragment of intuitionistic linear logic. Inf. Comput. 110, 2, 327–365.CrossRefGoogle Scholar
Hodas, J. S. 1994. Logic programming in intuitionistic linear logic: Theory, design, and implementation. Ph.D. thesis, University of Pennsylvania, Department of Computer and Information Science.CrossRefGoogle Scholar
Hodas, J. S. and Tamura, N. 2001. lolliCop – A linear logic implementation of a lean connection-method theorem prover for first-order classical logic. In Proceedings of IJCAR: International Joint Conference on Automated Reasoning, Goré, R., Leitsch, A., and Nipkow, T., Eds. LNCS, vol. 2083. Springer, 670–684.Google Scholar
Hofmann, M. 1999. Semantical analysis of higher-order abstract syntax. In 14th Symposium on Logic in Computer Science. IEEE Computer Society Press, 204–213.Google Scholar
Howard, W. A. 1980. The formulae-as-type notion of construction, 1969. In To H. B. Curry: Essays in Combinatory Logic, Lambda Calculus, and Formalism, Seldin, J. P. and Hindley, R., Eds. Academic Press, New York, 479–490.Google Scholar
Howe, J. M. 1998. Proof Search Issues in Some Non-Classical Logics. Ph.D. thesis, University of St Andrews. Available as University of St Andrews Research Report CS/99/1.Google Scholar
Huet, G. and Lang, B. 1978. Proving and applying program transformations expressed with second-order patterns. Acta Informatica 11, 31–55.Google Scholar
Huet, G. P. 1973. A mechanization of type theory. In Proceedings of the 3rd International Joint Conference on Artificial Intelligence. William Kaufmann, 139–146.Google Scholar
Huet, G. P. 1975. A unification algorithm for typed λ-calculus. Theor. Comput. Sci. 1, 27–57.CrossRefGoogle Scholar
ISO.org. 2000. ISO/IEC 13211-2:2000: Information technology – Programming languages – Prolog – part 2: Modules.Google Scholar
Jaffar, J. and Lassez, J.-L. 1987. Constraint logic programming. In Proceedings of the 14th ACM Symposium on the Principles of Programming Languages. ACM.CrossRefGoogle Scholar
Jagadeesan, R., Nadathur, G. and Saraswat, V. 2005. Testing concurrent systems: An interpretation of intuitionistic logic. In FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science. LNCS, vol. 3821. Springer, Hyderabad, India, 517–528.Google Scholar
Kahn, G. 1987. Natural semantics. In Proceedings of the Symposium on Theoretical Aspects of Computer Science, Brandenburg, F.-J., Vidal-Naquet, G., and Wirsing, M., Eds. LNCS, vol. 247. Springer, 22–39.Google Scholar
Kanovich, M., Kuznetsov, S., Nigam, V. and Scedrov, A. 2019. Subexponentials in non-commutative linear logic. Math. Struct. Comput. Sci. 29, 8, 1217–1249.CrossRefGoogle Scholar
Kanovich, M. I. 1995. Petri nets, Horn programs, Linear Logic and vector games. Ann. Pure Appl. Log. 75, 1–2, 107–135.CrossRefGoogle Scholar
Kobayashi, N. and Yonezawa, A. 1993. ACL - A concurrent linear logic programming paradigm. In Proceedings of the 1993 International Symposium on Logic Programming, D. Miller, Ed. Press, MIT, 279–294.Google Scholar
Kobayashi, N. and Yonezawa, A. 1994. Asynchronous communication model based on linear logic. Formal Aspects of Computing 3, 279–294.Google Scholar
Kowalski, R. A. 1979. Algorithm = Logic + Control. Communications of the Association for Computing Machinery 22, 424–436.CrossRefGoogle Scholar
Kowalski, R. 1974. Predicate logic as a programming language. Information Processing 74, 569–574.Google Scholar
Lambek, J. 1958. The mathematics of sentence structure. American Mathematical Monthly 65, 154–169.Google Scholar
Li, B. Z. 1994. A π-calculus specification of Prolog. In Proc. of European Symposium on Programming (ESOP 1994). LNCS, vol. 788. Springer, 379–393.Google Scholar
Liang, C. and Miller, D. 2007. Focusing and polarization in intuitionistic logic. In CSL 2007: Computer Science Logic, Duparc, J. and Henzinger, T. A., Eds. LNCS, vol. 4646. Springer, 451–465.Google Scholar
Liang, C. and Miller, D. 2009. Focusing and polarization in linear, intuitionistic, and classical logics. Theor. Comput. Sci. 410, 46, 4747–4768.CrossRefGoogle Scholar
Lifschitz, V. 1996. Foundations of logic programming. In Principles of Knowledge Representation, G. Brewka, Ed. Publications, CSLI, Stanford, California, 69–127.Google Scholar
Lifschitz, V. 2008. What is answer set programming? In Proceedings of the 23rd National Conference on Artificial Intelligence. Vol. 3. AAAI Press, 1594–1597.Google Scholar
Lincoln, P. 1995. Deciding provability of linear logic formulas. In Proceedings of the Workshop on Advances in Linear Logic, Girard, J.-Y., Lafont, Y., and Regnier, L., Eds. Cambridge University Press, New York, NY, USA, 197–210.Google Scholar
Lincoln, P. and Saraswat, V. 1993. Higher-order, linear, concurrent constraint programming. ftp://parcftp.xerox.com/pub/ccp/lcc/hlcc.dvi.CrossRefGoogle Scholar
Lipton, J. and Nieva, S. 2018. Kripke semantics for higher-order type theory applied to constraint logic programming languages. Theor. Comput. Sci. 712, 1–37.Google Scholar
Lisitsa, A. 2003. λleanTAP: Lean deduction in λProlog. Tech. Rep. ULCS-03-017, University of Liverpool, Department of Computer Science.Google Scholar
Lloyd, J. and Topor, R. 1984. Making Prolog more expressive. J. Log. Program. 1, 3 (Oct.), 225–240.CrossRefGoogle Scholar
Lloyd, J. W. and Shepherdson, J. C. 1991. Partial evaluation in logic programming. The J. Log. Program. 11, 3, 217–242.CrossRefGoogle Scholar
Loveland, D. W. 1970. A linear format for resolution. In Symposium on Automatic Demonstration. Number 125 in Lecture Notes in Mathematics. Springer Verlag, Berlin, 147–162.Google Scholar
Loveland, D. W. 1987. Near-Horn PROLOG. In Proceedings of the Fourth International Conference on Logic Programming, J.-L. Lassez, Ed. Press Series, MIT in Logic Programming. The MIT Press, Melbourne, 456–469.Google Scholar
Loveland, D. W. and Reed, D. W. 1991. A near-Horn Prolog for compilation. In Computational Logic - Essays in Honor of Alan Robinson, Lassez, J.-L. and Plotkin, G., Eds. MIT Press, 542–564.Google Scholar
Luckham, D. 1970. Refinement theorems in resolution theory. In Symposium on Automatic Demonstration. Number 125 in Lecture Notes in Mathematics. Springer Verlag, Berlin, 163–190.Google Scholar
Maier, D. and Warren, D. S. 1988. Computing with Logic: Logic Programming with Prolog. Addison-Wesley, Reading, MA.Google Scholar
Marek, W. and Truszczyński, M. 1993. Nonmonotonic Logics: Context-Dependent Reasoning. Berlin: Springer-Verlag.CrossRefGoogle Scholar
Martin-Löf, P. 1971. Hauptsatz for the intuitionistic theory of iterated inductive definitions. In Proceedings of the Second Scandinavian Logic Symposium, J. E. Fenstad, Ed. Studies in Logic and the Foundations of Mathematics, vol. 63. North-Holland, 179–216.Google Scholar
Martin-Löf, P. 1982. Constructive mathematics and computer programming. In Sixth International Congress for Logic, Methodology, and Philosophy of Science. North-Holland, Amsterdam, 153–175.CrossRefGoogle Scholar
McCarty, L. T. 1988a. Clausal intuitionistic logic I. Fixed point semantics. J. Log. Program. 5, 1–31.Google Scholar
McCarty, L. T. 1988b. Clausal intuitionistic logic II. Tableau proof procedure. J. Log. Program. 5, 93–132.Google Scholar
McDowell, R. and Miller, D. 2000. Cut-elimination for a logic with definitions and induction. Theor. Comput. Sci. 232, 91–119.Google Scholar
Michaylov, S. and Pfenning, F. 1992. Natural semantics and some of its meta-theory in Elf. In Extensions of Logic Programming, Eriksson, L.-H., Hallnäs, L., and Schroeder-Heister, P., Eds. LNCS, vol. 596. Springer, 299–344.Google Scholar
Miller, D. 1989. A logical analysis of modules in logic programming. J. Log. Program. 6, 1–2, 79–108.CrossRefGoogle Scholar
Miller, D. 1991a. A logic programming language with lambda-abstraction, function variables, and simple unification. J. Log. Comput. 1, 4, 497–536.CrossRefGoogle Scholar
Miller, D. 1991b. Proof theory as an alternative to model theory. Newsl. Assoc. Log. Program. 4, 3 (Aug.). Guest editorial.Google Scholar
Miller, D. 1992. Unification under a mixed prefix. J. Symb. Comput. 14, 4, 321–358.CrossRefGoogle Scholar
Miller, D. 1993. The π-calculus as a theory in linear logic: Preliminary results. In 3rd Workshop on Extensions to Logic Programming, Lamma, E. and Mello, P., Eds. LNCS, vol. 660. Springer, Bologna, Italy, 242–265.Google Scholar
Miller, D. 1994. A multiple-conclusion meta-logic. In 9th Symp. on Logic in Computer Science, S. Abramsky, Ed. Computer Society, IEEE, Paris, 272–281.Google Scholar
Miller, D. 1996. Forum: A multiple-conclusion specification logic. Theor. Comput. Sci. 165, 1, 201–232.CrossRefGoogle Scholar
Miller, D. 2003. Encryption as an abstract data-type: An extended abstract. In Proceedings of FCS’03: Foundations of Computer Security, I. Cervesato, Ed. ENTCS, vol. 84. Elsevier, 18–29.Google Scholar
Miller, D. 2004. Overview of linear logic programming. In Linear Logic in Computer Science, Ehrhard, T., Girard, J.-Y., Ruet, P., and Scott, P., Eds. London Mathematical Society Lecture Note, vol. 316. Cambridge University Press, 119–150.Google Scholar
Miller, D. 2006. Representing and reasoning with operational semantics. In Proceedings of IJCAR: International Joint Conference on Automated Reasoning, Furbach, U. and Shankar, N., Eds. LNAI, vol. 4130. Springer, 4–20.Google Scholar
Miller, D. 2008. A proof-theoretic approach to the static analysis of logic programs. In Reasoning in Simple Type Theory: Festschrift in Honor of Peter B. Andrews on His 70th Birthday. Number 17 in Studies in Logic. College Publications, 423–442.Google Scholar
Miller, D. 2017. Proof checking and logic programming. Form. Asp. Comput. 29, 3, 383–399.CrossRefGoogle Scholar
Miller, D. 2019. Mechanized metatheory revisited. J. Autom. Reason 63, 3, 625–665.CrossRefGoogle Scholar
Miller, D. 2021. Reciprocal influences between logic programming and proof theory. Philos. Technol. 34, 1 (Mar.), 75–104.CrossRefGoogle Scholar
Miller, D. and Nadathur, G. 1986a. Higher-order logic programming. In Proceedings of the Third International Logic Programming Conference, E. Shapiro, Ed. LNCS, vol. 225. Springer, London, 448–462.Google Scholar
Miller, D. and Nadathur, G. 1986b. Some uses of higher-order logic in computational linguistics. In Proceedings of the 24th Annual Meeting of the Association for Computational Linguistics. Association for Computational Linguistics, Morristown, New Jersey, 247–255.Google Scholar
Miller, D. and Nadathur, G. 2012. Programming with Higher-Order Logic. Cambridge University Press.CrossRefGoogle Scholar
Miller, D., Nadathur, G., Pfenning, F. and Scedrov, A. 1991. Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic 51, 1–2, 125–157.CrossRefGoogle Scholar
Miller, D. and Tiu, A. 2005. A proof theory for generic judgments. ACM Trans. on Computational Logic 6, 4 (Oct.), 749–783.Google Scholar
Milner, R. 1979. LCF: A way of doing proofs with a machine. In International Symposium on Mathematical Foundations of Computer Science. Springer, 146–159.Google Scholar
Milner, R., Tofte, M. and Harper, R. 1990. The Definition of Standard ML. MIT Press.Google Scholar
Minker, J. and Rajasekar, A. 1990. A fixpoint semantics for disjunctive logic programs. J. Log. Program. 9, 1, 45–74.CrossRefGoogle Scholar
Mints, G. and Tyugu, E. 1990. Propositional logic programming and Priz system. J. Log. Program. 9, 2&3, 179–193.Google Scholar
Mitchell, J. C. and Moggi, E. 1991. Kripke-style models for typed lambda calculus. Ann. Pure Appl. Log. 51, 1–2, 99–124.Google Scholar
Nadathur, G. 1987. A higher-order logic as the basis for logic programming. Ph.D. thesis, University of Pennsylvania.Google Scholar
Nadathur, G. 1993. A proof procedure for the logic of hereditary Harrop formulas. J. Autom. Reason. 11, 1, 115–145.CrossRefGoogle Scholar
Nadathur, G. 1998. Uniform provability in classical logic. J. Log. Comput. 8, 2, 209–229.CrossRefGoogle Scholar
Nadathur, G. 2000. Correspondences between classical, intuitionistic and uniform provability. Theor. Comput. Sci. 232, 273–298.CrossRefGoogle Scholar
Nadathur, G. 2005. A treatment of higher-order features in logic programming. Theory Pract. Log. Program. 5, 3, 305–354.CrossRefGoogle Scholar
Nadathur, G. and Loveland, D. 1995. Uniform proofs and disjunctive logic programming. In 10th Symposium on Logic in Computer Science, D. Kozen, Ed. IEEE Computer Society Press, San Diego, California, 148–155.Google Scholar
Nadathur, G. and Loveland, D. W. 1998. Proof procedures for logic programming. In Handbook of Logic in Artificial Intelligence and Logic Programming, Gabbay, D. M., Hogger, C. J., and Robinson, J. A., Eds. Vol. 5. Clarendon Press, Oxford, 163–234.Google Scholar
Nadathur, G. and Miller, D. 1988. An Overview of λProlog. In Fifth International Logic Programming Conference. MIT Press, Seattle, 810–827.Google Scholar
Nadathur, G. and Miller, D. 1990. Higher-order Horn clauses. J. ACM 37, 4, 777–814.Google Scholar
Nadathur, G. and Mitchell, D. J. 1999. System description: Teyjus – A compiler and abstract machine based implementation of λProlog. In 16th Conference on Automated Deduction (CADE), H. Ganzinger, Ed. LNAI, vol. 1632. Springer, Trento, 287–291.Google Scholar
Nadathur, G. and Pfenning, F. 1992. The type system of a higher-order logic programming language. In Types in Logic Programming, F. Pfenning, Ed. Press, MIT, 245–283.Google Scholar
Necula, G. C. 1997. Proof-carrying code. In Conference Record of the 24th Symposium on Principles of Programming Languages 97. ACM, Paris, France, 106–119.Google Scholar
Negri, S. and von Plato, J. 2001. Structural Proof Theory. Cambridge University Press.CrossRefGoogle Scholar
Nigam, V. 2009. Exploiting non-canonicity in the sequent calculus. Ph.D. thesis, Ecole Polytechnique.Google Scholar
Nigam, V. and Miller, D. 2009. Algorithmic specifications in linear logic with subexponentials. In ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP). ACM, 129–140.Google Scholar
Nigam, V., Olarte, C. and Pimentel, E. 2017. On subexponentials, focusing and modalities in concurrent systems. Theor. Comput. Sci. 693, 35–58.CrossRefGoogle Scholar
Nigam, V., Pimentel, E. and Reis, G. 2011. Specifying proof systems in linear logic with subexponentials. In Proceedings of the Fifth Logical and Semantic Frameworks, with Applications Workshop (LSFA 2010). ENTCS, vol. 269. Elsevier, 109–123.Google Scholar
Nipkow, T. 1993. Functional unification of higher-order patterns. In 8th Symp. on Logic in Computer Science, M. Vardi, Ed. IEEE, 64–74.Google Scholar
O’Keefe, R. A. 1990. The Craft of Prolog. MIT Press.Google Scholar
Olarte, C., Nigam, V. and Pimentel, E. 2015. Subexponential concurrent constraint programming. Theor. Comput. Sci. 606, 98–120.CrossRefGoogle Scholar
Ono, H. 1998. Proof-theoretic methods in nonclassical logic. an introduction. In Theories of Types and Proofs, Takahashi, M., Okada, M., and Dezani-Ciancaglini, M., Eds. Mathematical Society of Japan Memoirs, vol. 2. Mathematical Society of Japan, 207–254.Google Scholar
Otten, J. and Bibel, W. 2003. leanCoP: lean connection-based theorem proving. J. of Symbolic Computation 36, 1–2, 139–161.CrossRefGoogle Scholar
Paulson, L. C. 1989. The foundation of a generic theorem prover. J. of Automated Reasoning 5, 363–397.CrossRefGoogle Scholar
Perlis, A. J. 1982. Epigrams on programming. ACM SIGPLAN Notices 17, 9 (Sept.), 7–13.CrossRefGoogle Scholar
Pettorossi, A. and Proietti, M. 1994. Transformation of logic programs: Foundations and techniques. J. of Logic Programming 19/20, 261–320.CrossRefGoogle Scholar
Pfenning, F. 1988. Partial polymorphic type inference and higher-order unification. In Proceedings of the ACM Lisp and Functional Programming Conference. ACM.CrossRefGoogle Scholar
Pfenning, F. 1989. Elf: A language for logic definition and verified metaprogramming. In 4th Symp. on Logic in Computer Science. IEEE, Monterey, CA, 313–321.Google Scholar
Pfenning, F. 1991. Logic programming in the LF logical framework. In Logical Frameworks, Huet, G. and Plotkin, G., Eds. Cambridge University Press, 149–181.CrossRefGoogle Scholar
Pfenning, F. and Elliott, C. 1988. Higher-order abstract syntax. In Proceedings of the ACM-SIGPLAN Conference on Programming Language Design and Implementation. ACM Press, 199–208.Google Scholar
Pfenning, F. and Schürmann, C. 1999. System description: Twelf – A meta-logical framework for deductive systems. In 16th Conference on Automated Deduction (CADE), H. Ganzinger, Ed. LNAI, vol. 1632. Springer, Trento, 202–206.Google Scholar
Pientka, B. 2002. A proof-theoretic foundation for tabled higher-order logic programming. In 18th International Conference on Logic Programming (ICLP 2002), P. J. Stuckey, Ed. LNCS, vol. 2401. Springer, 271–286.Google Scholar
Pitts, A. M. 2003. Nominal logic, A first order theory of names and binding. Inform. Comput. 186, 2, 165–193.CrossRefGoogle Scholar
Plotkin, G. D. 1981. A structural approach to operational semantics. DAIMI FN-19, Aarhus University, Aarhus, Denmark. Sept.Google Scholar
Plotkin, G. D. 2004. A structural approach to operational semantics. J. Log. Algebr. Program. 60–61, 17–139.Google Scholar
Polakow, J. 2001. Ordered linear logic and applications. Ph.D. thesis, Department of Computer Science, Caregnie Mellon.Google Scholar
Polakow, J. and Pfenning, F. 1999. Natural deduction for intuitionistic non-commutative linear logic. In Proceedings of the 4th International Conference on Typed Lambda Calculi and Applications (TLCA 1999), J.-Y. Girard, Ed. LNCS, vol. 1581. Springer, 295–309.Google Scholar
Pym, D. and Harland, J. 1994. The uniform proof-theoretic foundation of linear logic programming. J. Log. Comput. 4, 2, 175–207.CrossRefGoogle Scholar
Qi, X., Gacek, A., Holte, S., Nadathur, G. and Snow, Z. 2015. The Teyjus system – version 2. http://teyjus.cs.umn.edu/.Google Scholar
Retoré, C. 1997. Pomset logic: A non-commutative extension of classical linear logic. In Proceedings of TLCA. Vol. 1210. Springer, 300–318.Google Scholar
Robinson, J. A. 1965. A machine-oriented logic based on the resolution principle. J. ACM 12, 23–41.CrossRefGoogle Scholar
Ruet, P. and Fages, F. 1997. Concurrent constraint programming and non-commutative logic. In Proceedings of the 11 th Conference on Computer Science Logic, Nielsen, M. and Thomas, W., Eds. LNCS, vol. 1414. Springer.CrossRefGoogle Scholar
Saraswat, V. 1993. A brief introduction to linear concurrent constraint programming. Tech. rep., Xerox Palo Alto Research Center.CrossRefGoogle Scholar
Schroeder-Heister, P. 1991. Uniform proof-theoretic semantics for logical constants (abstract). J. Symb. Log. 56, 1142.Google Scholar
Schroeder-Heister, P. 1993. Rules of definitional reflection. In 8th Symp. on Logic in Computer Science, M. Vardi, Ed. Computer Society, IEEE Press, IEEE, 222–232.Google Scholar
Schubert, A. and Urzyczyn, P. 2018. First-order answer set programming as constructive proof search. Theory Pract. Log. Program. 18, 3-4, 673–690.Google Scholar
Schwichtenberg, H. 2006. Minlog. In The Seventeen Provers of the World, F. Wiedijk, Ed. LNCS, vol. 3600. Springer, 151–157.Google Scholar
Scott, D. 1970. Outline of a mathematical theory of computation. In Proceedings, 4th Annual Princeton Conference on Information Sciences and Systems. Princeton University, 169–176. Also, Programming Research Group Technical Monograph PRG–2, Oxford University.Google Scholar
Simmons, R. J. and Pfenning, F. 2008. Linear logical algorithms. In 35th International Colloquium Automata, Languages and Programming (ICALP 2008), Aceto, L., Damgård, I., Goldberg, L. A., Halldórsson, M. M., Ingólfsdóttir, A., and Walukiewicz, I., Eds. LNCS, vol. 5126. Springer, 336–347.Google Scholar
Sørensen, M. H. and Urzyczyn, P. 2006. Lectures on the Curry-Howard Isomorphism . Studies in Logic, vol. 149. Elsevier.Google Scholar
Stampoulis, A. and Chlipala, A. 2018. Prototyping a functional language using higher-order logic programming: a functional pearl on learning the ways of λProlog/Makam. Proc. ACM Program. Lang. 2, ICFP, 93:1–93:30.Google Scholar
Statman, R. 1979. Intuitionistic propositional logic is polynomial-space complete. Theoretical Comput. Sci. 9, 67–72.CrossRefGoogle Scholar
Stickel, M. 1988. A PROLOG technology theorem prover: Implementation by an extended PROLOG compiler. J. Autom. Reason. 4, 4, 353–380.CrossRefGoogle Scholar
Stoy, J. E. 1977. Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory. MIT Press, Cambridge, MA.Google Scholar
Takahashi, M. 1967. A proof of cut-elimination theorem in simple type theory. J. Math. Soc. Jpn. 19, 399–410.Google Scholar
Takeuti, G. 1953. On a generalized logic calculus. Jpn. J. Math. 23, 39–96. Errata: ibid, vol. 24 (1954), 149–156.Google Scholar
Tärnlund, S.-A. 1977. Horn Clause Computability. BIT 17, 215–226.CrossRefGoogle Scholar
Tassi, E. 2018. Elpi: an extension language for Coq. CoqPL 2018: The Fourth International Workshop on Coq for Programming Languages.Google Scholar
Tassi, E. 2019. Deriving Proved Equality Tests in Coq-Elpi: Stronger Induction Principles for Containers in Coq. In 10th International Conference on Interactive Theorem Proving (ITP 2019), Harrison, J., O’Leary, J., and Tolmach, A., Eds. Leibniz International Proceedings in Informatics (LIPIcs), vol. 141. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 29:1–29:18.Google Scholar
Van Gelder, A., Ross, K. A. and Schilpf, J. S. 1991. The well-founded semantics for general logic programs. J. ACM 38, 3, 620–662.Google Scholar
Wadge, W. W. 1991. Higher-order Horn logic programming. In Proceedings of the 1991 International Symposium on Logic Programming. MIT Press, San Diego, California, USA, 289–303.Google Scholar
Wadler, P. 2003. Call-by-value is dual to call-by-name. In 8th International Conference on Functional Programming. ACM, New York, NY, 189–201.Google Scholar
Wang, Y. 2016. A higher-order abstract syntax approach to the verified compilation of functional programs. Ph.D. thesis, University of Minnesota.Google Scholar
Wang, Y. and Nadathur, G. 2016. A higher-order abstract syntax approach to verified transformations on functional programs. In Programming Languages and Systems. ESOP 2016, P. Thiemann, Ed. LNCS, vol. 9632. Springer, 752–779.Google Scholar
Wansing, H. 2002. Sequent systems for modal logics. In Handbook of Philosophical Logic, Volume VIII, 2 ed., Gabbay, D. M. and Guenthner, F., Eds. Kluwer Academic Publishers, Amsterdam, 61–146.Google Scholar
Warren, D. H. D. 1982. Higher-order extensions to Prolog: Are they needed? In Machine Intelligence 10. Halsted Press, Chicester, England, 441–454.Google Scholar
Warren, D. H. D. 1983. An abstract Prolog instruction set. Tech. Rep. 309, SRI International.Google Scholar
Warren, D. S. 2018. Top-down and Bottom-up Evaluation Procedurally Integrated. Theory Pract. Log. Program 18, 3-4, 706–721.Google Scholar
Whalen, M. W. 2005. Trustworthy translation for the requirements state machine language without events. Ph.D. thesis, University of Minnesota.Google Scholar
Wielemaker, J., Schrijvers, T., Triska, M., and Lager, T. 2012. SWI-Prolog. Theory Pract. Log. Program 12, 1-2, 67–96.CrossRefGoogle Scholar
Wos, L. and McCune, W. 1991. Automated theorem proving and logic programming: A natural symbiosis. J. Log. Program. 11, 1–53.Google Scholar
Zamov, N. K. and Sharonov, V. I. 1971. On a class of strategies for the resolution method. In Studies in Constructive Mathematics and Mathematical Logic, Part III, A. O. Slisenko, Ed. Number 16 in Seminars in Mathematics, V.A. Steklov Mathematical Institute, Leningrad. Consultants Bureau, New York, 26–31. Translated from Russian by J. S. Wood.Google Scholar