| 1. |
- Wehr, Dominik, 1998, et al.
(författare)
-
Material Dialogues forFirst-Order Logic inConstructive Type Theory
- 2022
-
Ingår i: Logic, Language, Information, and Computation, 28th International Workshop, WoLLIC 2022, Iași, Romania, September 20–23, 2022, Proceedings / Editors: Agata Ciabattoni, Elaine Pimentel, Ruy J. G. B. de Queiroz. - Cham : Springer International Publishing. - 0302-9743 .- 1611-3349.
-
Konferensbidrag (refereegranskat)abstract
- Material dialogues are turn taking games which model debates about the satisfaction of logical formulas. A novel variant played over first-order structures gives rise to a notion of first-order satisfaction. We study the induced notion of validity for classical and intuitionistic first-order logic in the constructive setting of the calculus of inductive constructions. We prove that such material dialogue semantics for classical first-order logic admits constructive soundness and completeness proofs, setting it apart from standard model theoretic semantics of first-order logic. Furthermore, we prove that completeness with regards to intuitionistic material dialogues fails in constructive and classical settings. The results concerning classical material dialogues have been mechanized using the Coq interactive theorem prover.
|
|
| 2. |
- Afshari, Bahareh, 1981, et al.
(författare)
-
Abstract Cyclic Proofs
- 2024
-
Ingår i: Mathematical Structures in Computer Science. - 0960-1295 .- 1469-8072.
-
Tidskriftsartikel (refereegranskat)
|
|
| 3. |
- Afshari, Bahareh, 1981, et al.
(författare)
-
Abstract Cyclic Proofs (Extended abstract)
- 2022
-
Ingår i: Lecture Notes in Computer Science, 28th International Workshop on Logic, Language, Information and Computation, Iași, Romania, September 20–23, 2022, Proceedings. - Cham : Springer. - 0302-9743 .- 1611-3349. - 9783031152979
-
Konferensbidrag (refereegranskat)abstract
- Cyclic proof systems permit derivations that are finite graphs in contrast to conventional derivation trees. The soundness of such proofs is ensured by a condition on the paths through the derivation graph, known as the global trace condition. To give a uniform treatment of such cyclic proof systems, Brotherston proposed an abstract notion of trace. We extend Brotherston’s approach into a category theoretical rendition of cyclic derivations, advancing the framework in two ways: First, we introduce activation algebras which allow for a more natural formalisation of trace conditions in extant cyclic proof systems. Second, accounting for the composition of trace information allows us to derive novel results about cyclic proofs, such as introducing the Ramsey trace condition.
|
|
| 4. |
|
|
| 5. |
- Leigh, Graham E., 1983, et al.
(författare)
-
From GTC to RESET : Generating reset proof systems from cyclic proof systems
- 2024
-
Ingår i: ANNALS OF PURE AND APPLIED LOGIC. - 0168-0072 .- 1873-2461. ; 175:10
-
Tidskriftsartikel (refereegranskat)abstract
- We consider cyclic proof systems in which derivations are graphs rather than trees. Such systems typically come with a condition that isolates which derivations are admitted as proofs, known as the soundness condition . This soundness condition frequently takes the form of either a global trace condition, a property dependent on all infinite paths in the proof -graph, or a reset condition, a 'local' condition depending on the simple cycles only which, as a result, is typically stable under more proof transformations. In this article we present a general method for constructing cyclic proof systems with reset conditions from systems with global trace conditions. In contrast to previous approaches, this method of generation is entirely independent of logic's semantics, only relying on combinatorial aspects of the notion of 'trace' and 'progress'. We apply this method to present reset proof systems for three cyclic proof systems from the literature: cyclic arithmetic, cyclic G & ouml;del's T and cyclic tableaux for the modal mu -calculus. (c) 2024 The Author(s). Published by Elsevier B.V. This is an open access article under the CC BY license (http://creativecommons .org /licenses /by /4 .0/).
|
|
| 6. |
- Wehr, Dominik, 1998, et al.
(författare)
-
Material dialogues for first-order logic in constructive type theory: extended version
- 2023
-
Ingår i: Mathematical Structures in Computer Science. - 0960-1295.
-
Tidskriftsartikel (refereegranskat)abstract
- Dialogues are turn-taking games which model debates about the satisfaction of logical formulas. A novel variant played over first-order structures gives rise to a notion of first-order satisfaction. We study the induced notion of validity for classical and intuitionistic first-order logic in the constructive setting of the calculus of inductive constructions. We prove that such material dialogue semantics for classical first-order logic admits constructive soundness and completeness proofs, setting it apart from standard model-theoretic semantics of first-order logic. Furthermore, we prove that completeness with regard to intuitionistic material dialogues fails in both constructive and classical settings. As an alternative, we propose material dialogues played over Kripke structures. These Kripke material dialogues exhibit constructive completeness when restricting to the negative fragment. The results concerning classical material dialogues have been mechanized using the Coq interactive theorem prover.
|
|
| 7. |
- Wehr, Dominik, 1998
(författare)
-
Representation matters in cyclic proof theory
- 2023
-
Licentiatavhandling (övrigt vetenskapligt/konstnärligt)abstract
- Cyclic proof systems allowderivations whose underlying structure is a finite graph, rather than a well-founded tree. The soundness of cyclic proofs is usually ensured by imposing additional conditions beyond well-formedness. Distinct cyclic representations of the same logic can be obtained by combining the same stock of logical rules with different soundness conditions. This thesis is a compilation of work in cyclic proof theory with a focus on the representation of cyclic proofs. The perspective is justified two-fold: First, the choice of representation of cyclic proofs has significant impact on proof theoretic investigations of cyclic proofs, dictating the effort required to derive desired results. Second, arguments which focus on the ‘cyclic’ aspects of cyclic proof systems, such as proof representations, rather than relying on specifics of logics, transfer more easily between different logics. This thesis makes several contributions to the field of cyclic proof theory. First, we present a method for generating reset proof systems, a representation of cyclic proofs which has previously been key to proof theoretic investigations, from cyclic proof systems with global trace conditions, by far the most common representation of cyclic proofs in the literature. Because the method is presented in a generic manner, this yields reset proof systems for most logics considered in the cyclic proof theory literature. Second, we transfer a proof method of the equivalence of cyclic and ‘inductive’ proof systems, first employed by Sprenger and Dam, to the setting of Heyting and Peano arithmetic. Whereas previous proofs of this equivalence for arithmetic theories have relied on intricate arithmetical formalisations of meta-mathematical concepts, our proof operates at the level of cyclic proof representations. Third, using insights into the aforementioned proof method, we put forward a novel form of representation for cyclic proof systems which is of interest to cyclic proof theory beyond the proving of cyclic-inductive equivalences.
|
|
