Simple consequence relations
From MaRDI portal
The approach to characterize propositional logical connectives by rules for sequent calculi was developed mainly via natural deduction. The author uses multiple sequent calculi with definitions like: internal disjunction is a binary connective \(+\) such that \(X\vdash Y,A,B\) iff \(X\vdash Y,A+B\). In this way he characterizes multiplicative and additive connectives of Girard's linear logic as well as other connectives. There is a hope to apply this framework for implementing logical systems on computers using the LF system. A good test for such an implementation is to try to prove translations (into the system considered) of sufficiently difficult intuitionistic formulas.
Recommendations
Cites work
- A constructive analysis of RM
- A logic covering undefinedness in program proofs
- A natural extension of natural deduction
- Display logic
- Gentzenizing Schroeder-Heister's natural extension of natural deduction
- scientific article; zbMATH DE number 3936465 (Why is no real title available?)
- scientific article; zbMATH DE number 3941494 (Why is no real title available?)
- scientific article; zbMATH DE number 4055576 (Why is no real title available?)
- scientific article; zbMATH DE number 3497860 (Why is no real title available?)
- scientific article; zbMATH DE number 3504935 (Why is no real title available?)
- scientific article; zbMATH DE number 1028818 (Why is no real title available?)
- scientific article; zbMATH DE number 1028823 (Why is no real title available?)
- scientific article; zbMATH DE number 1852923 (Why is no real title available?)
- scientific article; zbMATH DE number 1852926 (Why is no real title available?)
- scientific article; zbMATH DE number 3275554 (Why is no real title available?)
- scientific article; zbMATH DE number 3333259 (Why is no real title available?)
- scientific article; zbMATH DE number 3358455 (Why is no real title available?)
- scientific article; zbMATH DE number 3077773 (Why is no real title available?)
- On an implication connective of RM
- Proof theory
- Relevant entailment—semantics and formal systems
- Rules and Derived Rules
- Semantical investigations in Heyting's intuitionistic logic
- Sequent-systems for modal logic
- The lambda calculus. Its syntax and semantics. Rev. ed.
- The semantics and proof theory of linear logic
- What is Logic?
Cited in
(62)- Multi-valued semantics: why and how
- The semantics and proof theory of linear logic
- Nonmonotonic reasoning, preferential models and cumulative logics
- Gentzen-type systems, resolution and tableaux
- Set-theoretical and other elementary models of the \(\lambda\)-calculus
- Structured theory presentations and logic representations
- A generalization of analytic deduction via labelled deductive systems. I: Basic substructural logics
- Proof-search in type-theoretic languages: An introduction
- Eliminating disjunctions by disjunction elimination
- A note on contraction-free logic for validity
- Combining classical logic, paraconsistency and relevance
- Anti-intuitionism and paraconsistency
- On negation: Pure local rules
- Logical systems for structured specifications.
- On the formalization of the modal -calculus in the calculus of inductive constructions
- What is a logic translation?
- Structural weakening and paradoxes
- Hopeful monsters: a note on multiple conclusions
- Basing sequent systems on exclusive-or
- Proof theory of paraconsistent weak Kleene logic
- A simple logical matrix and sequent calculus for Parry's logic of analytic implication
- A survey of nonstandard sequent calculi
- What is the logic of inference?
- Logicality, double-line rules, and modalities
- Metainferences from a proof-theoretic perspective, and a hierarchy of validity predicates
- The original sin of proof-theoretic semantics
- Naive truth and naive logical properties
- Consequence relations and admissible rules
- Does the implication elimination rule need a minor premise?
- A Critical Overview of the Most Recent Logics of Grounding
- What is a paraconsistent logic?
- ST, LP and tolerant metainferences
- Relevant connexive logic
- Tutorial on admissible rules in Gudauri
- Strict canonical constructive systems
- A defeasible reasoning model of inductive concept learning from examples and communication
- Reasoning with different levels of uncertainty
- scientific article; zbMATH DE number 3916222 (Why is no real title available?)
- Does the deduction theorem fail for modal logic?
- What is an inference rule?
- A natural deduction approach to dynamic logic
- Logical consequence and the paradoxes
- Equivalences between logics and their representing type theories
- Disjoint logics
- THE JACOBSON RADICAL OF A PROPOSITIONAL THEORY
- A fully classical truth theory characterized by substructural means
- A practical implementation of simple consequence relations using inductive definitions
- Consequence-inconsistency interrelation: in the framework of paraconsistent logics
- Eliminating disjunctions by disjunction elimination
- An abstract approach to consequence relations
- A family of metainferential logics
- On extensibility of proof checkers
- The expressive power of Structural Operational Semantics with explicit assumptions
- Axiomatizing non-deterministic many-valued generalized consequence relations
- Relevant consequence relations: an invitation
- Using typed lambda calculus to implement formal systems on a machine
- Theo: An interactive proof development system
- Carnap's (categoricity) problem
- Invertibility in Sequent Calculi
- Cut-elimination and quantification in canonical systems
- Inferences and metainferences in \(\mathsf{ST}\)
- The proof monad
This page was built for publication: Simple consequence relations
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q809992)
