A browser-based automated reasoner for Input/Output Logics
Input/Output (I/O) logics have been devised by Makinson and van der Torre [1] as a class of formal systems for norm-based deontic reasoning. Intuitively, they formalize the question what obligations can be detached (the output) from a given set of conditional norms and a specific situation (the input). It differs from other deontic logics in the sense that the norms themselves are not part of the object logic and hence do not carry truth values. Constrained I/O logic [2] addresses contrary-to-duty situations and other dilemmas.
The I/O Logic Workbench is aimed at providing a browser-based automated reasoning system for various I/O logics. In short, the system allows you to input a set of norms and an input (the description of the current situation), and provides automated means for inferring whether a certain formula can be derived as an obligation from this.
The graphical user interface consists of two main panels: The configuration panel (on the left) and the main panel (on the right).
In the left menu panel, a user can choose which out operation should be used for the reasoning process. Furthermore, a selection of semantic parameters can be accessed for the output operations. Fially, some example scenarios can be loaded using the respective buttons at the top left.
On the right side, the input A, the set of norms N and a prospective output
x can be entered. The input language is an ASCII representation of propositional logic,
where |, & and ~ denote disjunction, conjunction and negation,
respectively. There are no binding preferences between conjunction and disjunction,
so they have to be properly parenthesised. Atomic propositions are any sequence of letters,
e.g. a, abc or veryLongNameForMyAtomicProposition.
The literals T and F are interpreted as truth and falsehood, respectively.
An example formula is x & (c | d) & ~e.
The input A is a comma separated list of formulas (possibly empty), whereas the
set of norms N is, as usual, represented as a set of pairs. Every norm is entered
as a separate line in the text area. The prospective output x is a simple formula.
Use case 1: Checking a prospective output.
To check whether a formula is in the output set of the selected out operator, enter the respective
information for A, N and x and press "check given output".
Use case 2: Generating the output set.
To let the tool generate the complete output set, enter the respective
information for A and N (x is not required here)
and press "generate output set". The (infinite) output set is represented by its finite base.
Example: Cn(a,b,c) represents the set of all (classical) consequences of the set
{a,b,c}, including, e.g., a, a & b and a | (x & y).
The source code of the I/O Logic Workbench is open-source and freely available at GitHub. It is implemented as a client-side application in JavaScript, so that there is no need for any backend server infrastructure. Hence, it runs in every reasonably current browser, ready-to-use for conducting own experiments without any major installation or set-up.
Current version: see the GitHub project for more details.
The I/O Logic Workbench is licensed using the GNU GPL license (see LICENSE file), and uses third party libraries that are distributed under their own terms (see LICENSE-3RD-PARTIES file).