Cited By
View all- Férée HGiessen IGool SShillito I(2024)Mechanised Uniform Interpolation for Modal Logics K, GL, and iSLAutomated Reasoning10.1007/978-3-031-63501-4_3(43-60)Online publication date: 2-Jul-2024
Formalizing and Computing Propositional Quantifiers
Authors: 
Hugo Férée, Sam van GoolAuthors Info & Claims
Pages 148 - 158
Abstract
A surprising result of Pitts (1992) says that propositional quantifiers are definable internally in intuitionistic propositional logic (IPC). The main contribution of this paper is to provide a formalization of Pitts’ result in the Coq proof assistant, and thus a verified implementation of Pitts’ construction. We in addition provide an OCaml program, extracted from the Coq formalization, which computes propositional formulas that realize intuitionistic versions of ∃ p φ and ∀ p φ from p and φ.
References
[1]
Frédéric Blanqui, Solange Coupet-Grimal, William Delobel, Sébastien Hinderer, and Adam Koprowski. 2006. CoLoR: a Coq Library on Rewriting and termination. In Eighth International Workshop on Termination-WST 2006.
[2]
Sylvain Boulmé. 1996. A proof of Craig’s Interpolation Theorem in Coq. Edinburgh University.
[3]
Peter Chapman, James McKinna, and Christian Urban. 2008. Mechanising a Proof of Craig’s Interpolation Theorem for Intuitionistic Logic in Nominal Isabelle. In AISC Conference. 38–52.
[4]
Pierre Corbineau. 2003. First-Order Reasoning in the Calculus of Inductive Constructions. In TYPES Conference, Stefano Berardi, Mario Coppo, and Ferruccio Damiani (Eds.) (Lecture Notes in Computer Science, Vol. 3085). Springer, 162–177. https://doi.org/10.1007/978-3-540-24849-1_11
[5]
Nachum Dershowitz and Zohar Manna. 1979. Proving Termination with Multiset Orderings. Commun. ACM, 22, 8 (1979), aug, 465–476. issn:0001-0782 https://doi.org/10.1145/359138.359142
[6]
Floris van Doorn. 2015. Propositional Calculus in Coq. arXiv:1503.08744.
[7]
Roy Dyckhoff. 1992. Contraction-free sequent calculi for intuitionistic logic. Journal of Symbolic Logic, 57, 3 (1992), 795–807.
[8]
Roy Dyckhoff and Sara Negri. 2000. Admissibility of Structural Rules for Contraction-Free Systems of Intuitionistic Logic. The Journal of Symbolic Logic, 65, 4 (2000).
[9]
Malvin Gattinger. 2022. A Verified Proof of Craig Interpolation for Basic Modal Logic via Tableaux in Lean. In Advances in Modal Logic.
[10]
S. Ghilardi and M. Zawadowski. 2002. Sheaves, Games, and Model Completions. Springer, Dordrecht.
[11]
Hugo Herbelin. 1995. A λ -calculus structure isomorphic to Gentzen-style sequent calculus structure. In Computer Science Logic. Springer Berlin Heidelberg, 61–75.
[12]
Hugo Herbelin and Gyesik Lee. 2009. Forcing-Based Cut-Elimination for Gentzen-Style Intuitionistic Sequent Calculus. In WoLLIC conference (Lecture Notes in Computer Science, Vol. 5514). Springer, 209–217. https://doi.org/10.1007/978-3-642-02261-6_17
[13]
J. Hudelmaier. 1988. A Prolog program for intuitionistic logic. University of Tübingen. SNS-Bericht 88-28
[14]
Rosalie Iemhoff. 2019. Uniform interpolation and the existence of sequent calculi. Annals of Pure and Applied Logic, 170, 11 (2019), 102711. https://doi.org/10.1016/j.apal.2019.05.008
[15]
Tadeusz Litak. 2015. Formalisation of Wim Ruitenburg’s paper "On the Period of Sequences (An(p)) in Intuitionistic Propositional Calculus" (JSL 1984). https://git8.cs.fau.de/software/ruitenburg1984
[16]
Tadeusz Litak. 2017. The periodic sequence property. In TACL Conference. https://www.cs.cas.cz/tacl2017/abstracts/TACL_2017_paper_120.pdf
[17]
Andrew M. Pitts. 1992. On an Interpretation of Second Order Quantification in First Order Intuitionistic Propositional Logic. J. Symb. Log., 57, 1 (1992), 33–52.
[18]
Iris Project. 2022. The Iris 4.0 Reference. https://plv.mpi-sws.org/iris/appendix-4.0.pdf
[19]
Tom Ridge. 2006. Craig’s Interpolation Theorem formalised and mechanised in Isabelle/HOL. arXiv:cs/0607058
[20]
W. Ruitenburg. 1984. On the period of sequences (an(p)) in intuitionistic propositional calculus. Journal of Symbolic Logic, 49, 3 (1984), 892–899.
[21]
N. N. Vorobev. 1970. A new algorithm for derivability in the constructive propositional calculus. Amer. Math. Soc. Transl., 94 (1970), 37–71. Translated from the 1952 Russian original
Index Terms
- Formalizing and Computing Propositional Quantifiers
Recommendations
Evidence Algorithm and Inference Search in First-Order Logics
In the early 1970s, in Kiev, research on automated theorem proving started in the framework of the so-called Evidence Algorithm (EA) programme, having some general features with the Mizar project and, in particular, being oriented to the development of ...
Denotational Semantics for Modal Systems S3---S5 Extended by Axioms for Propositional Quantifiers and Identity
There are logics where necessity is defined by means of a given identity connective: $${\square\varphi := \varphi\equiv\top}$$ := ($${\top}$$ is a tautology). On the other hand, in many standard modal logics the concept of propositional identity (PI) $${...
Hypersequent Calculi for Modal Logics Extending S4
New Frontiers in Artificial IntelligenceAbstractIn this paper, we introduce hypersequent calculi for some modal logics extending S4 modal logic. In particular, we uniformly characterize hypersequent calculi for S4, S4.2, S4.3, S5 in terms of what are called “external modal structural rules” for ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
January 2023
347 pages
ISBN:9798400700262
DOI:10.1145/3573105
- General Chairs:
- Robbert Krebbers,
- Dmitriy Traytel,
- Program Chairs:
- Brigitte Pientka,
- Steve Zdancewic
Copyright © 2023 ACM.
Publication rights licensed to ACM. ACM acknowledges that this contribution was authored or co-authored by an employee, contractor or affiliate of a national government. As such, the Government retains a nonexclusive, royalty-free right to publish or reproduce this article, or to allow others to do so, for Government purposes only.
Sponsors
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 11 January 2023
Check for updates
Author Tags
Qualifiers
- Research-article
Conference
CPP '23
Sponsor:
CPP '23: 12th ACM SIGPLAN International Conference on Certified Programs and Proofs
January 16 - 17, 2023
MA, Boston, USA
Acceptance Rates
Overall Acceptance Rate 18 of 26 submissions, 69%
Upcoming Conference
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 58Total Downloads
- Downloads (Last 12 months)17
- Downloads (Last 6 weeks)0
Reflects downloads up to 16 Nov 2024
Other Metrics
Citations
Cited By
View all- Férée HGiessen IGool SShillito I(2024)Mechanised Uniform Interpolation for Modal Logics K, GL, and iSLAutomated Reasoning10.1007/978-3-031-63501-4_3(43-60)Online publication date: 2-Jul-2024
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in