Uniform proofs as a foundation for logic programming
From MaRDI portal
DOI10.1016/0168-0072(91)90068-WzbMATH Open0721.03037MaRDI QIDQ2640596FDOQ2640596
Authors: Gopalan Nadathur, Frank Pfenning, Dale Miller, Andre Scedrov 
Publication date: 1991
Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)
Recommendations
Glivenko classesunificationHorn clausesPROLOGHerbrand universeHarrop formulasabstract logic programming languageuniform proofCut-free Gentzen-type systemssurvey of implemented applications
Cut-elimination and normal-form theorems (03F05) Logic programming (68N17) Mechanization of proofs and logical operations (03B35)
Cites Work
- HORNLOG: A graph-based interpreter for general Horn clauses
- Title not available (Why is that?)
- Title not available (Why is that?)
- The Semantics of Predicate Logic as a Programming Language
- Concerning formulas of the types A→B ν C,A →(Ex)B(x) in intuitionistic formal systems
- A kripke-kleene semantics for logic programs*
- Title not available (Why is that?)
- Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
- N-Prolog: An extension of Prolog with hypothetical implications. I.
- Contributions to the Theory of Logic Programming
- A logical analysis of modules in logic programming
- Proving and applying program transformations expressed with second-order patterns
- A unification algorithm for typed \(\overline\lambda\)-calculus
- Natural deduction as higher-order resolution
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Higher-order Horn clauses
Cited In (only showing first 100 items - show all)
- From axioms to synthetic inference rules via focusing
- Uniform closures: Order-theoretically reconstructing logic program semantics and abstract domain refinements
- Kripke semantics for higher-order type theory applied to constraint logic programming languages
- Structural cut elimination. I: Intuitionistic and classical logic
- A new framework for declarative programming
- Translating propositional extended conjunctions of Horn clauses into Boolean circuits
- Bounded linear-time temporal logic: a proof-theoretic investigation
- Temporal BI: proof system, semantics and translations
- A framework for proof systems
- Parsing/theorem-proving for logical grammar \textit{CatLog3}
- Least and Greatest Fixed Points in Linear Logic
- Proofs as computations in linear logic
- On the intuitionistic force of classical search
- Declarative compilation for constraint logic programming
- Non-commutative proof construction: a constraint-based approach
- Linearizing intuitionistic implication
- A semantics for \(\lambda \)Prolog
- Focused and Synthetic Nested Sequents
- Logic Programming
- Proof-theoretic and higher-order extensions of logic programming
- An improved proof-theoretic compilation of logic programs
- Representing scope in intuitionistic deductions
- Focussing and proof construction
- Proof checking and logic programming
- Proof checking and logic programming
- On the extension of logic programming with negation through uniform proofs
- The Abella Interactive Theorem Prover (System Description)
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
- Nominal abstraction
- Programming in metric temporal logic
- Forum: A multiple-conclusion specification logic
- A uniform semantic proof for cut-elimination and completeness of various first and higher order logics.
- On the algebraic structure of declarative programming languages
- The \(\lambda \)-calculus and the unity of structural proof theory
- Automatic verification of secrecy properties for linear logic specifications of cryptographic protocols
- Possible worlds and resources: The semantics of \(\mathbf{BI}\)
- Higher-order substitutions
- Correspondences between classical, intuitionistic and uniform provability
- Permutability of proofs in intuitionistic sequent calculi
- Uniform schemata for proof rules
- Resolution calculus for the first order linear logic
- Cut-elimination for a logic with definitions and induction
- Linear concurrent constraint programming: Operational and phase semantics
- Relating state-based and process-based concurrency through linear logic (full-version)
- Efficient resource management for linear logic proof search
- A proof-theoretic treatment of \(\lambda \)-reduction with cut-elimination: \(\lambda \)-calculus as a logic programming language
- Towards Ludics Programming: Interactive Proof Search
- A Constructive Semantic Approach to Cut Elimination in Type Theories with Axioms
- A game semantics for disjunctive logic programming
- A proof procedure for the logic of hereditary Harrop formulas
- A focused approach to combining logics
- Rewriting calculus with(out) types
- A note on the proof theory of the \(\lambda \Pi\)-calculus
- Abstractions of uniform proofs
- Focusing and polarization in linear, intuitionistic, and classical logics
- A two-level logic approach to reasoning about computations
- Title not available (Why is that?)
- Implementing tactics and tacticals in a higher-order logic programming language
- A uniform proof-theoretic foundation for abstract paraconsistent logic programming
- On the expressivity of minimal generic quantification
- Higher-order unification with dependent function types
- MELL in the calculus of structures
- Constraint logic programming with a relational machine
- Abstract deduction and inferential models for type theory
- Unifying theories for logic programming
- The Logic of Bunched Implications
- A coinductive approach to proof search through typed lambda-calculi
- Relating state-based and process-based concurrency through linear logic
- On structuring proof search for first order linear logic
- The practice of logical frameworks
- Reasoning in Abella about structural operational semantics specifications
- Formalizing a Constraint Deductive Database Language Based on Hereditary Harrop Formulas with Negation
- Proof relevant corecursive resolution
- Goal-oriented proof-search in natural deduction for intuitionistic propositional logic
- A survey of GCLA: a definitional approach to logic programming
- A logical semantics for depth-first Prolog with ground negation
- Structural focalization
- Focused proof-search in the logic of bunched implications
- Mechanized metatheory revisited
- Multi-focused proofs with different polarity assignments
- A proposal for broad spectrum proof certificates
- Operational semantics of resolution and productivity in Horn clause logic
- Correct answers for first order logic
- Non-commutative logic. III: Focusing proofs.
- Proof-terms for classical and intuitionistic resolution
- Formalizing operational semantic specifications in logic
- Term-Generic Logic
- An extended constraint deductive database: theory and implementation
- A proof theoretic view of spatial and temporal dependencies in biochemical systems
- Reductive logic, proof-search, and coalgebra: a perspective from resource semantics
- Focusing Gentzen's LK proof system
- An ecumenical notion of entailment
- A Proof-theoretic Analysis of Goal-directed Provability
- The new normal: we cannot eliminate cuts in coinductive calculi, but we can explore them
- Title not available (Why is that?)
- Encoding a dependent-type λ-calculus in a logic programming language
- Logical approximation for program analysis
- COCHIS: stable and coherent implicits
- Some applications of Gentzen's proof theory in automated deduction
- Tactic theorem proving with refinement-tree proofs and metavariables
Uses Software
This page was built for publication: Uniform proofs as a foundation for logic programming
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2640596)
