Uniform proofs as a foundation for logic programming
From MaRDI portal
Recommendations
Cites work
- scientific article; zbMATH DE number 3978351 (Why is no real title available?)
- scientific article; zbMATH DE number 3988745 (Why is no real title available?)
- scientific article; zbMATH DE number 4053062 (Why is no real title available?)
- scientific article; zbMATH DE number 3275554 (Why is no real title available?)
- scientific article; zbMATH DE number 3300581 (Why is no real title available?)
- scientific article; zbMATH DE number 3333259 (Why is no real title available?)
- A kripke-kleene semantics for logic programs*
- A logical analysis of modules in logic programming
- A unification algorithm for typed \(\overline\lambda\)-calculus
- Concerning formulas of the types A→B ν C,A →(Ex)B(x) in intuitionistic formal systems
- Contributions to the Theory of Logic Programming
- HORNLOG: A graph-based interpreter for general Horn clauses
- Higher-order Horn clauses
- 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.
- Natural deduction as higher-order resolution
- Proving and applying program transformations expressed with second-order patterns
- The Semantics of Predicate Logic as a Programming Language
Cited in
(only showing first 100 items - show all)- A uniform semantic proof for cut-elimination and completeness of various first and higher order logics.
- Automatic verification of secrecy properties for linear logic specifications of cryptographic protocols
- On the intuitionistic force of classical search
- Parsing/theorem-proving for logical grammar \textit{CatLog3}
- Efficient resource management for linear logic proof search
- A two-level logic approach to reasoning about computations
- An improved proof-theoretic compilation of logic programs
- scientific article; zbMATH DE number 3988745 (Why is no real title available?)
- Focussing and proof construction
- The practice of logical frameworks
- Possible worlds and resources: The semantics of \(\mathbf{BI}\)
- Abstract deduction and inferential models for type theory
- Proof checking and logic programming
- Higher-order unification with dependent function types
- Unifying theories for logic programming
- From axioms to synthetic inference rules via focusing
- The Logic of Bunched Implications
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
- Permutability of proofs in intuitionistic sequent calculi
- Proof checking and logic programming
- On the extension of logic programming with negation through uniform proofs
- On the algebraic structure of declarative programming languages
- A Constructive Semantic Approach to Cut Elimination in Type Theories with Axioms
- MELL in the calculus of structures
- Resolution calculus for the first order linear logic
- A proof-theoretic treatment of \(\lambda \)-reduction with cut-elimination: \(\lambda \)-calculus as a logic programming language
- Non-commutative proof construction: a constraint-based approach
- Cut-elimination for a logic with definitions and induction
- A game semantics for disjunctive logic programming
- Kripke semantics for higher-order type theory applied to constraint logic programming languages
- Nominal abstraction
- Focused and Synthetic Nested Sequents
- Programming in metric temporal logic
- A coinductive approach to proof search through typed lambda-calculi
- Declarative compilation for constraint logic programming
- Rewriting calculus with(out) types
- Correspondences between classical, intuitionistic and uniform provability
- Focusing and polarization in linear, intuitionistic, and classical logics
- Proofs as computations in linear logic
- Linear concurrent constraint programming: Operational and phase semantics
- The \(\lambda \)-calculus and the unity of structural proof theory
- A uniform proof-theoretic foundation for abstract paraconsistent logic programming
- The Abella Interactive Theorem Prover (System Description)
- A note on the proof theory of the \(\lambda \Pi\)-calculus
- Implementing tactics and tacticals in a higher-order logic programming language
- Structural cut elimination. I: Intuitionistic and classical logic
- Relating state-based and process-based concurrency through linear logic
- Linearizing intuitionistic implication
- Bounded linear-time temporal logic: a proof-theoretic investigation
- Abstractions of uniform proofs
- A new framework for declarative programming
- On structuring proof search for first order linear logic
- Forum: A multiple-conclusion specification logic
- Reasoning in Abella about structural operational semantics specifications
- Logic Programming
- Proof-theoretic and higher-order extensions of logic programming
- Higher-order substitutions
- Temporal BI: proof system, semantics and translations
- Constraint logic programming with a relational machine
- Relating state-based and process-based concurrency through linear logic (full-version)
- Translating propositional extended conjunctions of Horn clauses into Boolean circuits
- Uniform schemata for proof rules
- A proof procedure for the logic of hereditary Harrop formulas
- Representing scope in intuitionistic deductions
- A focused approach to combining logics
- On the expressivity of minimal generic quantification
- A semantics for \(\lambda \)Prolog
- Formalizing a Constraint Deductive Database Language Based on Hereditary Harrop Formulas with Negation
- Uniform closures: Order-theoretically reconstructing logic program semantics and abstract domain refinements
- Towards Ludics Programming: Interactive Proof Search
- Uniform provability in classical logic
- A framework for proof systems
- Theorem proving for conditional logics: CondLean and GOALDUCK
- Formalizing operational semantic specifications in logic
- COCHIS: stable and coherent implicits
- A proposal for broad spectrum proof certificates
- A resource aware semantics for a focused intuitionistic calculus
- scientific article; zbMATH DE number 1497841 (Why is no real title available?)
- Logical approximation for program analysis
- Term-Generic Logic
- Reductive logic, proof-search, and coalgebra: a perspective from resource semantics
- Focusing Gentzen's LK proof system
- A Proof-theoretic Analysis of Goal-directed Provability
- An ecumenical notion of entailment
- Tactic theorem proving with refinement-tree proofs and metavariables
- Proof relevant corecursive resolution
- An Analytic Propositional Proof System on Graphs
- The new normal: we cannot eliminate cuts in coinductive calculi, but we can explore them
- Proof certificates for equality reasoning
- Proof-search in type-theoretic languages: An introduction
- The calculus of constructions as a framework for proof search with set variable instantiation
- Definite Formulae, Negation-as-Failure, and the Base-Extension Semantics of Intuitionistic Propositional Logic
- Goal-oriented proof-search in natural deduction for intuitionistic propositional logic
- Encoding a dependent-type λ-calculus in a logic programming language
- Partial proof terms in the study of idealized proof search
- Operational semantics of resolution and productivity in Horn clause logic
- Formalizing adequacy: a case study for higher-order abstract syntax
- Correct answers for first order logic
- Non-commutative logic. III: Focusing proofs.
- Towards substructural property-based testing
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)
