rocq-docs-inquisitive-logic
About
Welcome to the Inquisitive Logic project website!
This project formalizes inquisitive logic in Rocq, based on the work of e.g. Ivano Ciardelli.
The current focus lies on (bounded) inquisitive first-order logic, therefore providing a formalization of the basic syntax (using arity types), support and truth semantics, followed by the formalization of a sequent calculus by Litak/Sano whose corresponding paper (Bounded inquistive logics: Sequent calculi and schematic validity) got accepted for TABLEAUX 2025.
The theory is located under theories/.
Some concrete instances of type classes (e.g. signatures) are located under instances/.
We also provide some examples (examples/) in order to demonstrate the implemented theory.
This is an open source project, licensed under the BSD 3-Clause “New” or “Revised” License.
Get the code
The current stable release of Inquisitive Logic can be downloaded from GitHub.
Documentation
The coqdoc presentation of the source files can be browsed here
Related publications, if any, are listed below.
- Inquisitive Logic: Consequence and Inference in the Realm of Questions doi:10.1007/978-3-031-09706-5
- Coherence in inquisitive first-order logic doi:10.1016/j.apal.2022.103155
- Bounded inquisitive logic: Sequent calculi and schematic validity
Help and contact
- Report issues on GitHub
Authors and contributors
- Max Ole Elliger (initial)
Other versions
Other versions stored here are listed in the following: