Reasoning about Intuitionistic Computation Tree Logic

In this paper, we define an intuitionistic version of Computation Tree Logic. After explaining the semantic features of intuitionistic logic, we examine how these characteristics can be interesting for formal verification purposes. Subsequently, we define the syntax and semantics of our intuitionistic version of CTL and study some simple properties of the so obtained logic. We conclude by demonstrating that some fixed-point axioms of CTL are not valid in the intuitionistic version of CTL we have defined.

Logical Semantics, Dialogical Argumentation, and Textual Entailment

In this chapter, we introduce a new dialogical system for first order classical logic which is close to natural language argumentation, and we prove its completeness with respect to usual classical validity. We combine our dialogical system with the Grail syntactic and semantic parser developed by the second author in order to address automated textual entailment, that is, we use it for deciding whether or not a sentence is a consequence of a short text. This work-which connects natural language semantics and argumentation with dialogical logic-can be viewed as a step towards an inferentialist view of natural language semantics.