Nonmonotonic Reasoning, Expectations Orderings, and Conceptual Spaces

In Gärdenfors and Makinson (Artif Intell 65(2):197–245, 1994) and Gärdenfors (Knowledge representation and reasoning under uncertainty, Springer-Verlag, 1992) it was shown that it is possible to model nonmonotonic inference using a classical consequence relation plus an expectation-based ordering of formulas. In this article, we argue that this framework can be significantly enriched by adopting a conceptual spaces-based analysis of the role of expectations in reasoning. In particular, we show that this can solve various epistemological issues that surround nonmonotonic and default logics. We propose some formal criteria for constructing and updating expectation orderings based on conceptual spaces, and we explain how to apply them to nonmonotonic reasoning about objects and properties.

Completeness for the Classical Antecedent Fragment of Inquisitive First-Order Logic

Inquisitive first order logic "Equation missing" is an extension of first order classical logic, introducing questions and studying the logical relations between questions and quantifiers. It is not known whether "Equation missing" is recursively axiomatizable, even though an axiomatization has been found for fragments of the logic (Ciardelli, 2016). In this paper we define the $$\mathsf {ClAnt}$$ ClAnt —classical antecedent—fragment, together with an axiomatization and a proof of its strong completeness. This result extends the ones presented in the literature and introduces a new approach to study the axiomatization problem for fragments of the logic.

Performability of Actions

Action theory may be regarded as a theoretical foundation of AI, because it provides in a logically coherent way the principles of performing actions by agents. But, more importantly, action theory offers a formal ontology mainly based on set-theoretic constructs. This ontology isolates various types of actions as structured entities: atomic, sequential, compound, ordered, situational actions etc., and it is a solid and non-removable foundation of any rational activity. The paper is mainly concerned with a bunch of issues centered around the notion of performability of actions. It seems that the problem of performability of actions, though of basic importance for purely practical applications, has not been investigated in the literature in a systematic way thus far. This work, being a companion to the book as reported (Czelakowski in Freedom and enforcement in action. Elements of formal action theory, Springer 2015), elaborates the theory of performability of actions based on relational models and formal constructs borrowed from formal lingusistics. The discussion of performability of actions is encapsulated in the form of a strict logical system "Equation missing". This system is semantically defined in terms of its intended models in which the role of actions of various types (atomic, sequential and compound ones) is accentuated. Since due to the nature of compound actions the system "Equation missing" is not finitary, other semantic variants of "Equation missing" are defined. The focus in on the system "Equation missing" of performability of finite compound actions. An adequate axiom system for "Equation missing" is defined. The strong completeness theorem is the central result. The role of the canonical model in the proof of the completeness theorem is highlighted. The relationship between performability of actions and dynamic logic is also discussed.

Verification and Strategy Synthesis for Coalition Announcement Logic

Coalition announcement logic (CAL) is one of the family of the logics of quantified announcements. It allows us to reason about what a coalition of agents can achieve by making announcements in the setting where the anti-coalition may have an announcement of their own to preclude the former from reaching its epistemic goals. In this paper, we describe a PSPACE-complete model checking algorithm for CAL that produces winning strategies for coalitions. The algorithm is implemented in a proof-of-concept model checker.