Related papers: Automated Reasoning over Deontic Action Logics wit…
Systems of deontic logic suffer either from being too expressive and therefore hard to mechanize, or from being too simple to capture relevant aspects of normative reasoning. In this article we look for a suitable way in between: the…
The paper is a contribution both to the theoretical foundations and to the actual construction of efficient automatizable proof procedures for non-classical logics. We focus here on the case of finite-valued logics, and exhibit: (i) a…
In this paper we present a theorem proving methodology for a restricted but significant fragment of the conditional language made up of (boolean combinations of) conditional statements with unnested antecedents. The method is based on the…
Deontic logic is a very well researched branch of mathematical logic and philosophy. Various kinds of deontic logics are discussed for different application domains like argumentation theory, legal reasoning, and acts in multi-agent…
Often, we assume that an action is permitted simply because it is not explicitly forbidden; or, similarly, that an action is forbidden simply because it is not explicitly permitted. This kind of assumptions appear, e.g., in autonomous…
We introduce the Deontic Action Model Logic (DAML), a dynamic modal framework for reasoning about obligations over actions in multi-agent systems. DAML extends the epistemic Action Model Logic by incorporating deontic evaluation mechanisms…
We study the satisfiability problem of symbolic finite automata and decompose it into the satisfiability problem of the theory of the input characters and the monadic second-order theory of the indices of accepted words. We use our…
We present a tableau calculus for reasoning in fragments of natural language. We focus on the problem of pronoun resolution and the way in which it complicates automated theorem proving for natural language processing. A method for…
A number of flexible tactic-based logical frameworks are nowadays available that can implement a wide range of mathematical theories using a common higher-order metalanguage. Used as proof assistants, one of the advantages of such powerful…
In our previous research, we provided a reasoning system (called LeSAC) based on argumentation theory to provide legal support to designers during the design process. Building on this, this paper explores how to provide designers with…
Non-normal modal logics, interpreted on neighbourhood models which generalise the usual relational semantics, have found application in several areas, such as epistemic, deontic, and coalitional reasoning. We present here preliminary…
It is widely acknowledged that function symbols are an important feature in answer set programming, as they make modeling easier, increase the expressive power, and allow us to deal with infinite domains. The main issue with their…
We present a multi-modal action logic with first-order modalities, which contain terms which can be unified with the terms inside the subsequent formulas and which can be quantified. This makes it possible to handle simultaneously time and…
In this paper we combine Answer Set Programming (ASP) with Dynamic Linear Time Temporal Logic (DLTL) to define a temporal logic programming language for reasoning about complex actions and infinite computations. DLTL extends propositional…
A semantic tableau method, called an argumentation tableau, that enables the derivation of arguments, is proposed. First, the derivation of arguments for standard propositional and predicate logic is addressed. Next, an extension that…
In this work we suggest the use of a set-theoretical interpretation of semantic tableaux for teaching propositional logic. If the student has previous notions of basic set theory, this approach to semantical tableaux can clarify her the way…
This paper provides a set of cut-free complete sequent-style calculi for deontic STIT ('See To It That') logics used to formally reason about choice-making, obligations, and norms in a multi-agent setting. We leverage these calculi to write…
Recently, the description logic LE-ALC was introduced for reasoning in the semantic environment of the enriched formal contexts, and a tableaux algorithm was developed for checking the consistency of ABoxes in this logic. In this paper, we…
We consider the problem of implementing deontic modal logic. We show how (deontic) modal operators can be elegantly and directly expressed using default negation (negation-as-failure) and strong negation present in answer set programming…
The rise of powerful AI technology for a range of applications that are sensitive to legal, social, and ethical norms demands decision-making support in presence of norms and regulations. Normative reasoning is the realm of deontic logics,…