相关论文: Constructive Modalities with Provability Smack

We consider a logic used to describe sets of configurations of distributed systems, whose network topologies can be changed at runtime, by reconfiguration programs. The logic uses inductive definitions to describe networks with an unbounded…

Recent advances in programming languages study and design have established a standard way of grounding computational systems representation in category theory. These formal results led to a better understanding of issues of control and…

Continuous first-order logic is used to apply model-theoretic analysis to analytic structures (e.g. Hilbert spaces, Banach spaces, probability spaces, etc.). Classical computable model theory is used to examine the algorithmic structure of…

Game Logic is an excellent setting to study proofs-about-programs via the interpretation of those proofs as programs, because constructive proofs for games correspond to effective winning strategies to follow in response to the opponent's…

We axiomatize the provability logic of $\HA$ and prove its decidability. Furthermore, we axiomatize the preservativity and relative admissibility relations for several modal logics extending iK4. A principal technical tool is the…

Evaluating conjunctive queries and solving constraint satisfaction problems are fundamental problems in database theory and artificial intelligence, respectively. These problems are NP-hard, so that several research efforts have been made…

The computational properties of modal and propositional dependence logics have been extensively studied over the past few years, starting from a result by Sevenster showing NEXPTIME-completeness of the satisfiability problem for modal…

In this paper we show that an intuitionistic theory for fixed points is conservative over the Heyting arithmetic with respect to a certain class of formulas. This extends partly the result of mine. The proof is inspired by the quick…

We propose to use Tarski's least fixpoint theorem as a basis to define recursive functions in the calculus of inductive constructions. This widens the class of functions that can be modeled in type-theory based theorem proving tool to…

Orthogonality is a notion based on the duality between programs and their environments used to determine when they can be safely combined. For instance, it is a powerful tool to establish termination properties in classical formal systems.…

We study a conservative extension of classical propositional logic distinguishing between four modes of statement: a proposition may be affirmed or denied, and it may be strong or classical. Proofs of strong propositions must be…

A class of models is presented, in the form of continuation monads polymorphic for first-order individuals, that is sound and complete for minimal intuitionistic predicate logic. The proofs of soundness and completeness are constructive and…

"Systems that Explain Themselves" appears a provocative wording, in particular in the context of mathematics education -- it is as provocative as the idea of building educational software upon technology from computer theorem proving. In…

This work presents a framework for control theory based on constructive analysis to account for discrepancy between mathematical results and their implementation in a computer, also referred to as computational uncertainty. In control…

The semantic paradoxes are associated with self-reference or referential circularity. However, there are infinitary versions of the paradoxes, such as Yablo's paradox, that do not involve this form of circularity. It remains an open…

Propositional formulas that are equivalent in intuitionistic logic, or in its extension known as the logic of here-and-there, have the same stable models. We extend this theorem to propositional formulas with infinitely long conjunctions…

Probabilistic programming is considered as a framework, in which basic components of cognitive architectures can be represented in unified and elegant fashion. At the same time, necessity of adopting some component of cognitive…

The importance of intuitionistic temporal logics in Computer Science and Artificial Intelligence has become increasingly clear in the last few years. From the proof-theory point of view, intuitionistic temporal logics have made it possible…

Computability theory is traditionally conceived as the theoretical basis of informatics. Nevertheless, numerous proposals transcend computability theory, in particular by emphasizing interaction of modules, or components, parts,…

Based on an analysis of the inference rules used, we provide a characterization of the situations in which classical provability entails intuitionistic provability. We then examine the relationship of these derivability notions to uniform…