A Survey of the Proof-Theoretic Foundations of Logic Programming (Q6063891): Difference between revisions

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