Cut-elimination for quantified conditional logic
From MaRDI portal
Publication:2363418
DOI10.1007/s10992-016-9403-0zbMath1417.03282OpenAlexW2431262575MaRDI QIDQ2363418
Publication date: 19 July 2017
Published in: Journal of Philosophical Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10992-016-9403-0
cut-eliminationsemantic embeddingclassical higher-order logiccut-simulationquantified conditional logics
Related Items
Extensional higher-order paramodulation in Leo-III ⋮ Designing normative theories for ethical and legal reasoning: \textsc{LogiKEy} framework, methodology, and tool support ⋮ BOUNDED-ANALYTIC SEQUENT CALCULI AND EMBEDDINGS FOR HYPERSEQUENT LOGICS ⋮ Automating free logic in HOL, with an experimental application in category theory
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- The higher-order prover \textsc{Leo}-II
- Analytic tableaux for higher-order logic with choice
- Combining and automating classical and non-classical logics in classical higher-order logics
- An example on the fundamental conjecture of \(GLC\)
- A first-order conditional logic for prototypical properties
- Basic conditional logic
- On first-order conditional logics
- Embedding and automating conditional logics in classical higher-order logic
- Quantified multimodal logics in simple type theory
- Sufficient conditions for cut elimination with complexity analysis
- A proof of cut-elimination theorem in simple type-theory
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
- Satallax: An Automatic Higher-Order Prover
- Multimodal and intuitionistic logics in simple type theory
- Interpolation for first order S5
- Intensional models for the theory of types
- Analytic Tableaux for Simple Type Theory and its First-Order Fragment
- Cut-Simulation and Impredicativity
- Syntactical and semantical properties of simple type theory
- Cut-elimination for simple type theory with an axiom of choice
- A sequent calculus and a theorem prover for standard conditional logics
- Higher-order semantics and extensionality
- Automated Deduction – CADE-20
- Hauptsatz for higher order logic
- A nonconstructive proof of Gentzen’s Hauptsatz for second order predicate logic
- Resolution in type theory
- General models, descriptions, and choice in type theory
- General models and extensionality
- A UNIFYING PRINCIPAL IN QUANTIFICATION THEORY
- First-order conditional logic for default reasoning revisited
- Reasoning with higher-order abstract syntax in a logical framework
- An Unsolvable Problem of Elementary Number Theory
- Completeness in the theory of types
- Generic Modal Cut Elimination Applied to Conditional Logics
- Proof theory
