A Survey of the Proof-Theoretic Foundations of Logic Programming
From MaRDI portal
Publication:6063891
DOI10.1017/s1471068421000533arXiv2109.01483OpenAlexW3216378269MaRDI QIDQ6063891
No author found.
Publication date: 12 December 2023
Published in: Theory and Practice of Logic Programming (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/2109.01483
Cites Work
- Linear logic
- Nominal abstraction
- Forum: A multiple-conclusion specification logic
- Kripke semantics for higher-order type theory applied to constraint logic programming languages
- The lambda calculus. Its syntax and semantics. Rev. ed.
- Kripke-style models for typed lambda calculus
- Lectures on the Curry-Howard isomorphism
- Subexponential concurrent constraint programming
- A logical characterization of forward and backward chaining in the inverse method
- Focusing and polarization in linear, intuitionistic, and classical logics
- Foundation of logic programming based on inductive definition
- A Prolog technology theorem prover: Implementation by an extended Prolog compiler
- Unification under a mixed prefix
- A unification algorithm for typed \(\overline\lambda\)-calculus
- Proving and applying program transformations expressed with second-order patterns
- Intuitionistic propositional logic is polynomial-space complete
- Implementing tactics and tacticals in a higher-order logic programming language
- A proof procedure for the logic of hereditary Harrop formulas
- Logic programming in a fragment of intuitionistic linear logic
- A logical semantics for depth-first Prolog with ground negation
- IeanCOP: lean connection-based theorem proving
- Correspondences between classical, intuitionistic and uniform provability
- Efficient resource management for linear logic proof search
- Cut-elimination for a logic with definitions and induction
- A semantic framework for proof evidence
- Hybrid and subexponential linear logics
- The polarized \(\lambda\)-calculus
- Edinburgh LCF. A mechanized logic of computation
- The foundation of a generic theorem prover
- Linear concurrent constraint programming: Operational and phase semantics
- A structural approach to operational semantics
- Nominal logic, a first order theory of names and binding
- A mathematical definition of full Prolog
- Petri nets, Horn programs, linear logic and vector games
- lean\(T^ AP\): Lean tableau-based deduction
- Non-commutative logic. I: The multiplicative fragment
- Mechanized metatheory revisited
- A proof theory for model checking
- A two-level logic approach to reasoning about computations
- On subexponentials, focusing and modalities in concurrent systems
- Translating between implicit and explicit versions of proof
- On structuring proof search for first order linear logic
- A proof of cut-elimination theorem in simple type-theory
- Proof checking and logic programming
- Uniform proofs as a foundation for logic programming
- A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs
- Programming with Higher-Order Logic
- SWI-Prolog
- The Duality of Computation under Focus
- A fixpoint semantics for disjunctive logic programs
- A Proof-Theoretic Approach to Logic Programming. I. Clauses as Rules
- The Mathematics of Sentence Structure
- Concerning formulas of the types A→B ν C,A →(Ex)B(x) in intuitionistic formal systems
- A treatment of higher-order features in logic programming
- An Adequate Compositional Encoding of Bigraph Structure in Linear Logic with Subexponentials
- ELPI: Fast, Embeddable, $$\lambda $$ Prolog Interpreter
- Higher-order Horn clauses
- Linear Logical Algorithms
- Classical and Intuitionistic Subexponential Logics Are Equally Expressive
- Focusing and Polarization in Intuitionistic Logic
- Representing and Reasoning with Operational Semantics
- N-Prolog: An extension of Prolog with hypothetical implications. I.
- Making prolog more expressive
- Linear-time algorithms for testing the satisfiability of propositional horn formulae
- N-Prolog: An extension of prolog with hypothetical implication. II. Logical foundations, and negation as failure
- Clausal intuitionistic logic I. fixed-point semantics
- Clausal intuitionistic logic II. tableau proof procedures
- Contributions to the Theory of Logic Programming
- Automated theorem proving and logic programming: a natural symbiosis
- A Proof-Theoretic Approach to Logic Programming
- A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
- Partial evaluation in logic programming
- A new constructive logic: classic logic
- Logic Programming with Focusing Proofs in Linear Logic
- A framework for defining logics
- HiLog: A foundation for higher-order logic programming
- Provability in Elementary Type Theory
- The Semantics of Predicate Logic as a Programming Language
- Horn clause computability
- Algorithm = logic + control
- From operational semantics to abstract machines
- A new definition of SLDNF-resolution
- A Uniform Proof-theoretic Investigation of Linear Logic Programming
- The well-founded semantics for general logic programs
- Logic programming and negation: A survey
- Transformation of logic programs: Foundations and techniques
- On goal-directed provability in classical logic
- Uniform provability in classical logic
- First-order Answer Set Programming as Constructive Proof Search
- Top-down and Bottom-up Evaluation Procedurally Integrated
- A logical analysis of modules in logic programming
- Functionality in Combinatory Logic
- Encryption as an abstract data-type
- Magically Constraining the Inverse Method Using Dynamic Polarity Assignment
- Higher-order unification with dependent function types
- Specifying Proof Systems in Linear Logic with Subexponentials
- Abella: A System for Reasoning about Relational Specifications
- Implementing type theory in higher order constraint logic programming
- Subexponentials in non-commutative linear logic
- Call-by-value is dual to call-by-name
- A proof theory for generic judgments
- A system of interaction and structure
- Logic Programming
- A Machine-Oriented Logic Based on the Resolution Principle
- An efficient context-free parsing algorithm
- Resolution in type theory
- A formulation of the simple theory of types
- The completeness of the first-order functional calculus
- FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
- Logical Approaches to Computational Barriers
- Focused linear logic and the \(\lambda\)-calculus
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
