Proof-search in type-theoretic languages: An introduction
From MaRDI portal
Publication:1575935
DOI10.1016/S0304-3975(99)00169-3zbMath0952.03006MaRDI QIDQ1575935
Publication date: 23 August 2000
Published in: Theoretical Computer Science (Search for Journal in Brave)
Functional programming and lambda calculus (68N18) Logic in computer science (03B70) Mechanization of proofs and logical operations (03B35) Proof theory in general (including proof-theoretic semantics) (03F03)
Related Items
Proof Search and Counter Model of Positive Minimal Predicate Logic, Cut Elimination in a Class of Sequent Calculi for Pure Type Systems
Uses Software
Cites Work
- Linear logic
- Forum: A multiple-conclusion specification logic
- Using typed lambda calculus to implement formal systems on a machine
- The lambda calculus. Its syntax and semantics. Rev. ed.
- Kripke-style models for typed lambda calculus
- Simple consequence relations
- On connections and higher-order logic
- The system \({\mathcal F}\) of variable types, fifteen years later
- Generalized algebraic theories and contextual categories
- The calculus of constructions
- Program development in constructive type theory
- Recursive programming with proofs
- A unification algorithm for typed \(\overline\lambda\)-calculus
- Resolution calculus for the first order linear logic
- Structured theory presentations and logic representations
- Logic programming in a fragment of intuitionistic linear logic
- Isabelle. A generic theorem prover
- Proof strategies in linear logic
- On proof normalization in linear logic
- A generalization of analytic deduction via labelled deductive systems. I: Basic substructural logics
- Completeness results for linear logic on Petri nets
- A linear logical framework
- On the intuitionistic force of classical search
- Encoding modal logics in logical frameworks
- Edinburgh LCF. A mechanized logic of computation
- Generating plans in linear logic. I: Actions as proofs
- The foundation of a generic theorem prover
- Untersuchungen über das logische Schliessen. I
- Productive use of failure in inductive proof
- TPS: A theorem-proving system for classical type theory
- Uniform proofs as a foundation for logic programming
- Quantales and (noncommutative) linear logic
- HYPERDOCTRINES, NATURAL DEDUCTION AND THE BECK CONDITION
- An interpretation of Martin-Löf's type theory in a type-free theory of propositions
- Logic and Computation
- Theorem Proving via General Matings
- On Matrices with Connections
- Phase semantics and sequent calculus for pure noncommutative classical linear propositional logic
- Logic Programming with Focusing Proofs in Linear Logic
- Contraction-free sequent calculi for intuitionistic logic
- A framework for defining logics
- A relevant analysis of natural deduction
- A specification logic for concurrent object-oriented programming
- The Logic of Bunched Implications
- A Complete Proof Synthesis Method for the Cube of Type Systems
- A Proof-theoretic Analysis of Goal-directed Provability
- A Uniform Proof-theoretic Investigation of Linear Logic Programming
- Games and full completeness for multiplicative linear logic
- Some Properties of Linear Logic Proved by Semantic Methods
- Proof-terms for classical and intuitionistic resolution
- Proof-search in intuitionistic logic based on constraint satisfaction
- A resolution theorem prover for intuitionistic logic
- From Petri nets to linear logic
- A logical analysis of modules in logic programming
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Kripke Resource Models of a Dependently-typed, Bunched -calculus
- Higher-order unification with dependent function types
- Representing proof transformations for program optimization
- Connection-based proof construction in linear logic
- Resource-distribution via Boolean constraints
- A UNIFICATION ALGORITHM FOR THE λΠ-CALCULUS
- A Machine-Oriented Logic Based on the Resolution Principle
- On closed categories of functors
- Linear Logic Proof Games and Optimization
