Uniform proofs as a foundation for logic programming

DOI10.1016/0168-0072(91)90068-WzbMath0721.03037MaRDI QIDQ2640596

Frank Pfenning, Gopalan Nadathur, Dale A. Miller, Andrej Scedrov

Publication date: 1991

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

PROLOG Horn clauses unification Glivenko classes Herbrand universe Harrop formulas abstract logic programming language uniform proof Cut-free Gentzen-type systems survey of implemented applications

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Cut-elimination and normal-form theorems (03F05) Logic programming (68N17)

Related Items

A Survey of the Proof-Theoretic Foundations of Logic Programming, An ecumenical notion of entailment, Refutation-aware Gentzen-style calculi for propositional until-free linear-time temporal logic, Towards substructural property-based testing, Definite Formulae, Negation-as-Failure, and the Base-Extension Semantics of Intuitionistic Propositional Logic, From axioms to synthetic inference rules via focusing, The Logic of Bunched Implications, MELL in the calculus of structures, Proof checking and logic programming, Operational semantics of resolution and productivity in Horn clause logic, A proof theoretic view of spatial and temporal dependencies in biochemical systems, A note on the proof theory of the \(\lambda \Pi\)-calculus, Higher-order unification with dependent function types, A semantics for \(\lambda \)Prolog, An Analytic Propositional Proof System on Graphs, Term-Generic Logic, Automatic verification of secrecy properties for linear logic specifications of cryptographic protocols, A resource aware semantics for a focused intuitionistic calculus, Formalizing adequacy: a case study for higher-order abstract syntax, A two-level logic approach to reasoning about computations, Programming in metric temporal logic, A game semantics for disjunctive logic programming, Structural Focalization, Temporal BI: proof system, semantics and translations, Logical approximation for program analysis, A logical semantics for depth-first Prolog with ground negation, Declarative Compilation for Constraint Logic Programming, Nominal abstraction, On the extension of logic programming with negation through uniform proofs, αCheck: A mechanized metatheory model checker, A new framework for declarative programming, Parsing/theorem-proving for logical grammar \textit{CatLog3}, A semantic framework for proof evidence, Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax, An extended constraint deductive database: theory and implementation, A focused approach to combining logics, Non-commutative logic. III: Focusing proofs., Unnamed Item, A Constructive Semantic Approach to Cut Elimination in Type Theories with Axioms, Goal-oriented proof-search in natural deduction for intuitionistic propositional logic, The Abella Interactive Theorem Prover (System Description), The New Normal: We Cannot Eliminate Cuts in Coinductive Calculi, But We Can Explore Them, A coinductive approach to proof search through typed lambda-calculi, Focused proof-search in the logic of bunched implications, Forum: A multiple-conclusion specification logic, Proof-terms for classical and intuitionistic resolution, Proof certificates for equality reasoning, Multi-focused proofs with different polarity assignments, A proof-theoretic treatment of λ-reduction with cut-elimination: λ-calculus as a logic programming language, On the intuitionistic force of classical search (Extended abstract), Constraint logic programming with a relational machine, Proof search with set variable instantiation in the Calculus of Constructions, An Improved Proof-Theoretic Compilation of Logic Programs, Kripke semantics for higher-order type theory applied to constraint logic programming languages, Relating State-Based and Process-Based Concurrency through Linear Logic, Translating propositional extended conjunctions of Horn clauses into Boolean circuits, Unnamed Item, Correct Answers for First Order Logic, Linearizing intuitionistic implication, Proof Checking and Logic Programming, Proofs as computations in linear logic, A framework for proof systems, Unnamed Item, Abstract deduction and inferential models for type theory, On structuring proof search for first order linear logic, Non-commutative proof construction: a constraint-based approach, Proof Relevant Corecursive Resolution, Relating state-based and process-based concurrency through linear logic (full-version), The \(\lambda \)-calculus and the unity of structural proof theory, 2004 Summer Meeting of the Association for Symbolic Logic, On the Expressivity of Minimal Generic Quantification, Reasoning in Abella about Structural Operational Semantics Specifications, Formalizing a Constraint Deductive Database Language Based on Hereditary Harrop Formulas with Negation, Least and Greatest Fixed Points in Linear Logic, Tactic theorem proving with refinement-tree proofs and metavariables, Focused and Synthetic Nested Sequents, COCHIS: Stable and coherent implicits, Representing scope in intuitionistic deductions, Theorem proving for conditional logics: CondLean and GOALDUCK, Permutability of proofs in intuitionistic sequent calculi, Formalizing Operational Semantic Specifications in Logic, A Proposal for Broad Spectrum Proof Certificates, Bounded linear-time temporal logic: a proof-theoretic investigation, Possible worlds and resources: The semantics of \(\mathbf{BI}\), Implementing type theory in higher order constraint logic programming, Constructing weak simulations from linear implications for processes with private names, On the algebraic structure of declarative programming languages, Focusing and polarization in linear, intuitionistic, and classical logics, Mechanized metatheory revisited, Encoding Generic Judgments, On the intuitionistic force of classical search, Correspondences between classical, intuitionistic and uniform provability, The calculus of constructions as a framework for proof search with set variable instantiation, Efficient resource management for linear logic proof search, Cut-elimination for a logic with definitions and induction, Proof-search in type-theoretic languages: An introduction, Focussing and proof construction, Towards Ludics Programming: Interactive Proof Search, Structural cut elimination. I: Intuitionistic and classical logic, Higher-order substitutions, Linear concurrent constraint programming: Operational and phase semantics, Implementing tactics and tacticals in a higher-order logic programming language, A proof procedure for the logic of hereditary Harrop formulas, Resolution calculus for the first order linear logic, The practice of logical frameworks

Uses Software

Hornlog

Cites Work