A Survey of the Proof-Theoretic Foundations of Logic Programming (Q6063891)

scientific article; zbMATH DE number 7776351

Language	Label	Description	Also known as
English	A Survey of the Proof-Theoretic Foundations of Logic Programming	scientific article; zbMATH DE number 7776351

Statements

instance of

scholarly article

0 references

title

A Survey of the Proof-Theoretic Foundations of Logic Programming (English)

0 references

published in

Theory and Practice of Logic Programming

0 references

publication date

12 December 2023

0 references

full work available at URL

https://arxiv.org/abs/2109.01483

0 references

MaRDI profile type

MaRDI publication profile

0 references

cites work

Non-commutative logic. I: The multiplicative fragment

0 references

Q3525697

0 references

Logic Programming with Focusing Proofs in Linear Logic

0 references

Q3357521

0 references

A logical semantics for depth-first Prolog with ground negation

0 references

Resolution in type theory

0 references

Provability in Elementary Type Theory

0 references

Q3343471

0 references

Logic programming and negation: A survey

0 references

A new definition of SLDNF-resolution

0 references

Contributions to the Theory of Logic Programming

0 references

Abella: A System for Reasoning about Relational Specifications

0 references

The lambda calculus. Its syntax and semantics. Rev. ed.

0 references

Q3077958

0 references

lean$T^ AP$: Lean tableau-based deduction

0 references

Q4783309

0 references

Translating between implicit and explicit versions of proof

0 references

A mathematical definition of full Prolog

0 references

Q4839029

0 references

Focused linear logic and the $\lambda$-calculus

0 references

Q5667469

0 references

On structuring proof search for first order linear logic

0 references

Q4215630

0 references

Q3821628

0 references

Q4944869

0 references

Efficient resource management for linear logic proof search

0 references

Classical and Intuitionistic Subexponential Logics Are Equally Expressive

0 references

Magically Constraining the Inverse Method Using Dynamic Polarity Assignment

0 references

A logical characterization of forward and backward chaining in the inverse method

0 references

An Adequate Compositional Encoding of Bigraph Structure in Linear Logic with Subexponentials

0 references

HiLog: A foundation for higher-order logic programming

0 references

Logic Programming

0 references

A semantic framework for proof evidence

0 references

A formulation of the simple theory of types

0 references

Q4317721

0 references

The Duality of Computation under Focus

0 references

Functionality in Combinatory Logic

0 references

Q4282602

0 references

Q4842975

0 references

Q3024831

0 references

Hybrid and subexponential linear logics

0 references

Q3327701

0 references

Linear-time algorithms for testing the satisfiability of propositional horn formulae

0 references

ELPI: Fast, Embeddable, $$\lambda $$ Prolog Interpreter

0 references

Logical Approaches to Computational Barriers

0 references

An efficient context-free parsing algorithm

0 references

Higher-order unification with dependent function types

0 references

The Semantics of Predicate Logic as a Programming Language

0 references

The polarized $\lambda$-calculus

0 references

Linear concurrent constraint programming: Operational and phase semantics

0 references

Implementing tactics and tacticals in a higher-order logic programming language

0 references

N-Prolog: An extension of prolog with hypothetical implication. II. Logical foundations, and negation as failure

0 references

N-Prolog: An extension of Prolog with hypothetical implications. I.

0 references

Nominal abstraction

0 references

A two-level logic approach to reasoning about computations

0 references

0 references

0 references

0 references

0 references

0 references

0 references

A new constructive logic: classic logic

0 references

Edinburgh LCF. A mechanized logic of computation

0 references

A system of interaction and structure

0 references

Implementing type theory in higher order constraint logic programming

0 references

Foundation of logic programming based on inductive definition

0 references

A Proof-Theoretic Approach to Logic Programming. I. Clauses as Rules

0 references

A Proof-Theoretic Approach to Logic Programming

0 references

From operational semantics to abstract machines

0 references

On goal-directed provability in classical logic

0 references

A framework for defining logics

0 references

Concerning formulas of the types <i>A→B</i> ν <i>C,A →(Ex)B(x)</i> in intuitionistic formal systems

0 references

A proof theory for model checking

0 references

The completeness of the first-order functional calculus

0 references

Logic programming in a fragment of intuitionistic linear logic

0 references

Q4539650

0 references

Proving and applying program transformations expressed with second-order patterns

0 references

A unification algorithm for typed $\overline\lambda$-calculus

0 references

FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science

0 references

Q3774923

0 references

Subexponentials in non-commutative linear logic

0 references

Petri nets, Horn programs, linear logic and vector games

0 references

Algorithm = logic + control

0 references

Q4051550

0 references

The Mathematics of Sentence Structure

0 references

Focusing and Polarization in Intuitionistic Logic

0 references

Focusing and polarization in linear, intuitionistic, and classical logics

0 references

Q4514010

0 references

Q4842970

0 references

Kripke semantics for higher-order type theory applied to constraint logic programming languages

0 references

Making prolog more expressive

0 references

Partial evaluation in logic programming

0 references

0 references

0 references

0 references

0 references

0 references

0 references

Clausal intuitionistic logic I. fixed-point semantics

0 references

Clausal intuitionistic logic II. tableau proof procedures

0 references

Cut-elimination for a logic with definitions and induction

0 references

A logical analysis of modules in logic programming

0 references

A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification

0 references

Unification under a mixed prefix

0 references

Forum: A multiple-conclusion specification logic

0 references

Encryption as an abstract data-type

0 references

Q4650578

0 references

Representing and Reasoning with Operational Semantics

0 references

Q3086788

0 references

Proof checking and logic programming

0 references

Mechanized metatheory revisited

0 references

Q3751042

0 references

Programming with Higher-Order Logic

0 references

Uniform proofs as a foundation for logic programming

0 references

A proof theory for generic judgments

0 references

Q3857731

0 references

A fixpoint semantics for disjunctive logic programs

0 references

Kripke-style models for typed lambda calculus

0 references

A proof procedure for the logic of hereditary Harrop formulas

0 references

Uniform provability in classical logic

0 references

Correspondences between classical, intuitionistic and uniform provability

0 references

A treatment of higher-order features in logic programming

0 references

Q4391447

0 references

Higher-order Horn clauses

0 references

Q2744125

0 references

On subexponentials, focusing and modalities in concurrent systems

0 references

Specifying Proof Systems in Linear Logic with Subexponentials

0 references

Subexponential concurrent constraint programming

0 references

Q4699355

0 references

IeanCOP: lean connection-based theorem proving

0 references

The foundation of a generic theorem prover

0 references

Transformation of logic programs: Foundations and techniques

0 references

Q3204068

0 references

Q4012879

0 references

Q4812964

0 references

Nominal logic, a first order theory of names and binding

0 references

A structural approach to operational semantics

0 references

Q2763630

0 references

Q4263877

0 references

A Uniform Proof-theoretic Investigation of Linear Logic Programming

0 references

Q3024915

0 references

A Machine-Oriented Logic Based on the Resolution Principle

0 references

Q4218945

0 references

First-order Answer Set Programming as Constructive Proof Search

0 references

Linear Logical Algorithms

0 references

Lectures on the Curry-Howard isomorphism

0 references

Intuitionistic propositional logic is polynomial-space complete

0 references

A Prolog technology theorem prover: Implementation by an extended Prolog compiler

0 references

Q3969890

0 references

A proof of cut-elimination theorem in simple type-theory

0 references

Q5822069

0 references

Horn clause computability

0 references

Q5875441

0 references

The well-founded semantics for general logic programs

0 references

Call-by-value is dual to call-by-name

0 references

A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs

0 references

Top-down and Bottom-up Evaluation Procedurally Integrated

0 references

SWI-Prolog

0 references

Automated theorem proving and logic programming: a natural symbiosis

0 references

Q5639372

0 references

Encoding a dependent-type λ-calculus in a logic programming language

0 references

Identifiers

arXiv ID

2109.01483

0 references

DOI

10.1017/s1471068421000533

0 references

Mathematics Subject Classification ID

0 references

0 references

0 references

Sitelinks

Mathematics(1 entry)

mardi Publication:6063891