Dialogical Logic [5,6] (also: dialogue logic) was originally proposed by Prof. Paul Lorenzen, who taught philosophy in Erlangen. Essential contributions are due to Kuno Lorenz, who later on became a professor of Philosophy in Saarbruecken. Native speakers of English are referred to Walter Felscher's articles on dialogical logic [2,3]. The latest and most comprehensive textbook (in German) has been written by Rüdiger Inhetveen [7].

The central idea of dialogical logic is to provide a pragmatic foundation of logic on a game-theoretic basis --- hence introducing semantics by a nutual agreement on moves ---, but it is as well suited for teaching logic. So, dialogical logic is commited to proof-theory; model theory does not play a foundational, but an illustrative role. Any successful proof in dialogical logic consists in the construction of a model, otherwise of a counter-example.

So, in dialogical logic, the validity of some formula F is examined
in *two person, perfect information games* . There are two
players moving alternatively, both having complete information of the
current situation of the game. The player who claims being able to
justify F is called the *proponent*, his adversary the
*opponent*.

The initial state, the *dialogue setting*, is determined by
a (possibly empty) set of *hypotheses* (introduced into the
game by the opponent) and a *thesis F*, the formula to be
shown valid, brought in by the proponent. The consecutive moves of
the dialogue game are *attacks* upon formulae asserted earlier
or *defences* against previous attacks. Some moves include the
introduction of formulae that might be subject to subsequent
attacks.

The legal moves that a player can perform are defined by so-called
*particle rules* and *frame rules*. For each logical
connective PHI a particle rule is given which specifies how attacks
upon moves asserting formulae that have PHI as main connective and
defences against such attacks have to be performed. The frame rules
organize the exchange of arguments, i.e., they impose restrictions on
when attacks and defences may take place in the dialogue. Depending
on the choice of frame rules, dialogical logic covers constructive
("intuitionistic") and classical logics as well.

A *dialogue game is won* by a player, if the other player
cannot perform any action that conforms with the dialogue rules. The
proponent is said to have a *winning strategy* for a formula F,
if he is able to win any game where formula F is the thesis (and a
given set of hypotheses) by appropriate choices of his statements. A
formula F is *valid*, if the proponent has a winning strategy
for F. Winning strategies might not be unique. Felscher [3,4]
presents a proof that the notion of winning strategies in dialogue
games (wrt. a well-defined set of dialogue rules) coincides with the
notion of provability in Gentzen's calculus LJ for intuitionistic
logic.

Recently, the idea of "logic games" as well as further approaches to dialogical logic have received a lot of attention, e.g. in publications by Barth, van Benthem, Hintikka, Hamblin, Krabbe, Mackenzie, Walton, and others.

We know of at least two implementations in the 1970s . One has been made in Erlangen by Gerrit Haas [4] at the Computer Science Institute (IMMD) on a PDP 7. Another implementation had been done (in Fortran on a Control Data 6600 and later ported to a CD 3300 in Erlangen) in Austin, Texas, where Lorenzen spent some time as a visiting professor (around 1970). Both systems implemented only the propositional part of dialogical logic.

Today, we know of no other implementation of Dialogical Logic except DiaLogic as presented here.

Later on, COLOSSEUM, a theorem prover for constructive predicate logic --- without an interactive mode to play dialogue games --- has been implemented in Prolog by Claus Zinn. For details, see here.

As far as we know, DiaLog is the first system which implements Dialogical Logic for propositional, full predicate, and modal logic. We had the following goals in mind:

- To better understand the dialogue calculus.
- To have a system for teaching purposes.
- To promote Dialogical Logic which is rather unknown in the Automatic Deduction community.

**Ad 1:** In the history of Dialogical Logic there has always been
a debate about the 'correct' specification of particle and frame
rules. It is the case, that different versions of frame and particle
rules lead to different logics. In the literature on Dialogical Logic,
numerous versions of them (mostly kept rather informal) can be found,
cf. [5,6]. In order to experiment with the dialogue rules, DiaLogic
offers the possibility to redefine both particle and frame rules by
means of a rule language. There are predefined rules for effective,
classical and modal logic.

**Ad 2:** Due to its friendly user interface, DiaLogic can
easily been used for teaching purposes. Dialogical Logic has been a
part of the curriculum for students of philosophy in Erlangen up to
now.

**Ad 3:** As documented in [0], the first full implementation of
Dialogical Logic has been made available to the Automated Deduction
community. Dialogical Logic is an interesting proof calculus which is
worth further investigation.

A description of the system for Dialogical Logic is provided in [0,1]. The latter description is in German and describes mostly implementation details. However, there is a chapter describing the use of DiaLogic. We have no further user or reference manuals available.

Here you see a snapshot of system run with its graphical user interface. The interface is divided into four parts:

- The pull-down menu,
- The dialogue tableau, split into an opponent and proponent component,
- The dialogue trace pane,
- The command interpreter pane.

System features are:

- fully automated proof search;
- interactive mode (user plays the proponent's part);
- Dialogue trace pane displaying all speech acts performed;
- Dialogue tableau showing the current status of the dialogue;
- Strategy grapher showing the winning strategy, if a proof has been found;
- Rule language to (re-)define particle and frame rules;
- Running with GUI on Unix and Windows platforms;
- Running without GUI (command line interface) also on any other platform, even DOS.

The system has been implemented in Scheme and Tk (the Scheme system STk offers both) by Jürgen Ehrensberger within his master's project under the supervision of Dr. Claus Zinn and Prof. Dr. Guenther Goerz at the Dept. of Computer Science / 8, (Artificial Intelligence) of the University of Erlangen-Nuremberg.

To run the DiaLogic system, you need a Scheme interpreter. We have
tested DiaLogic with several Scheme implementations obeying the R5RS
standard, in particular with SCM (Version
2a6) and STk
(Version 4.0.1). The Scheme Library SLIB is
required.
We **recommend strongly** to use the Berkeley modification of STk
4.0.1, called *UCB
Scheme*, version 4.0.1-ucb1.16, which is available for Linux,
Windows, and Mac OS X. It contains everything you need (including the
portable Scheme library SLIB) and is very easy to install.

- To run DiaLogic with a GUI you need either a Unix/Linux (X11) or Windows platform and STk.
- To run DiaLogic without the GUI (i.e., in command line mode), a DOS or any other platform providing a text-based shell, and SCM suffice.

[1] Ehrensberger, Jürgen.
* Ein System für Dialogische Logik. *
Diplomarbeit am Institut für Mathematische Maschinen und
Datenverarbeitung, Lehrstuhl Künstliche Intelligenz (Informatik 8).
Universität Erlangen-Nürnberg, 1996.
[PDF]

[2] Felscher, Walter.
* Dialogues, Strategies and Intuitionistic Provability *.
Annals of Pure and Applied Logic 28 (1985), 217--254

[3] Felscher, Walter.
* Dialogues as a Foundation for Intuitionistic Logic *
Handbook of Philosophical Logic. Vol. III.
Ed. by Dov M. Gabbay, and Franz Guenthner. Dordrecht: D. Reidel, 1986.
341--372.

[4] Haas, Gerrit.
* Programme zur dialogischen Logik *.
Arbeitsberichte des IMMD. Bd. 3, Nr. 4.
Universität Erlangen-Nürnberg, Oktober 1970.

[5] Lorenzen, Paul.
* Ein dialogisches Konstruktivitätskriterium *.
Infinitistic Methods. Proceedings of the Symposium on Foundations of
Mathematics (Warszawa 1959).
Oxford: Pergamon, 1961. 193--200.
(Reprinted in P. Lorenzen/K. Lorenz: * Dialogische Logik *. 9--16).

[6] Lorenzen Paul, and Lorenz, Kuno.
* Dialogische Logik *.
Darmstadt: Wissenschaftliche Buchgesellschaft, 1978.

[7] Inhetveen, Rüdiger.
* Logik -- Eine dialog-orientierte Einführung *.
Leipzig: Teubner, 2002.

Guenther Goerz Last modified: Sat Nov 25 16:58:16 CEST 2006