Geometrisation of first-order logic

DOI10.1017/BSL.2015.7MaRDI QIDQ2795295zbMATH OpenOpenAlexFDO

Authors Roy Dyckhoff, Sara Negri

Publication date 18 March 2016

Published in The Bulletin of Symbolic Logic (Search for Journal in Brave)

Full work available at URL http://hdl.handle.net/10023/6818

zbMATH Keywords

coherent implicationcoherent logicconservative extensiongeometric logicweakly positive formula

Mathematics Subject Classification ID

Classical first-order logic (03B10) Subsystems of classical logic (including intuitionistic logic) (03B20) Modal logic (including the logic of norms) (03B45) Basic properties of first-order languages and structures (03C07) Cut-elimination and normal-form theorems (03F05)

Recommendations

• Invited Talk: Coherentisation of First-Order Logic
• scientific article; zbMATH DE number 1354137
• Interpolation in extensions of first-order logic
• scientific article; zbMATH DE number 2097565
• Conservative extensions in modal logic

Cites work

• A coherent logic based geometry theorem prover capable of producing formal and readable proofs
• A FORMAL SYSTEM FOR EUCLID’SELEMENTS
• A Systematic Presentation of Quantified Modal Logics
• An Intuitionistic Axiomatisation of Real Closed Fields
• Aspects of topoi
• Contraction-free sequent calculi for geometric theories with an application to Barr's theorem
• Contraction-free sequent calculi for intuitionistic logic
• Gentzen-type systems, resolution and tableaux
• scientific article; zbMATH DE number 1003731 (Why is no real title available?)
• scientific article; zbMATH DE number 5539366 (Why is no real title available?)
• scientific article; zbMATH DE number 3787631 (Why is no real title available?)
• scientific article; zbMATH DE number 1531887 (Why is no real title available?)
• On the mechanization of the proof of Hessenberg's theorem in coherent logic
• Proof analysis in intermediate logics
• Proof analysis in modal logic
• Proofs and countermodels in non-classical logics
• The Church-Fitch knowability paradox in the light of structural proof theory
• Toposes without points

Cited in

(32)

• Algebraic geometry in first-order logic
• Formalizing mathematics in higher-order logic: A case study in geometric modelling
• A theory of duality in Euclidean geometry
• Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017
• Multicomponent proof-theoretic method for proving interpolation properties
• Proof-theoretic analysis of the logics of agency: the deliberative STIT
• Theorem proving as constraint solving with coherent logic
• From axioms to synthetic inference rules via focusing
• Formalizing Kant's rules. A logic of conditional imperatives and permissives
• The intensional side of algebraic-topological representation theorems
• Proof analysis for Lewis counterfactuals
• Inducing syntactic cut-elimination for indexed nested sequents
• Proving Craig and Lyndon interpolation using labelled sequent calculi
• Logical and set calculations in the framework of geometrical informatics paradigm
• Intuitionistic Decision Procedures Since Gentzen
• On Relating Theories: Proof-Theoretical Reduction
• Invited Talk: Coherentisation of First-Order Logic
• Geometrical structures and modal logic
• Undecidable First-Order Theories of Affine Geometries
• scientific article; zbMATH DE number 4120169 (Why is no real title available?)
• Geometric Rules in Infinitary Logic
• From mathematical axioms to mathematical rules of proof: recent developments in proof analysis
• scientific article; zbMATH DE number 7166981 (Why is no real title available?)
• Mechanising Gödel-Löb provability logic in HOL light
• No Speedup for Geometric Theories
• Automated generation of illustrated proofs in geometry and beyond
• Quantified modal logics: one approach to rule (almost) them all!
• Automated generation of illustrations for synthetic geometry proofs
• Designing a safe forward chaining tactic using productive proofs
• Theorem proving as constraint solving for coherent logic with function symbols
• Automated completion of statements and proofs in synthetic geometry: an approach based on constraint solving
• On geometric implications

Describes a project that uses

Uses Software

• ArgoCLP

This page was built for publication: Geometrisation of first-order logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2795295)