Publications on Labelled Tableaux
- Alberto Artosi, Paola Benassi, Guido Governatori, and
Antonino Rotolo.
-
Labelled proofs for quantified modal
logic.
In J.J. Alferes, L. M. Pereira, and E. Orlowska, editors, Logics in
Artificial Intelligence, number 1126 in LNAI, pages 70-86, Berlin, 1996.
Springer-Verlag.
Abstract:In this paper we describe a modal proof system arising
from the combination of a tableau-like classical system, which incorporates a
restricted (``analytic'') version of the cut rule, with a label formalism
which allows for a specialised, logic-dependent unification algorithm. The
system provides a uniform proof-theoretical treatment of first-order (normal)
modal logics with and without the Barcan Formula and/or its converse.
 
- Alberto Artosi, Paola Benassi, Guido Governatori, and
Antonino Rotolo.
-
Shakespearian modal logic: A labelled
treatment of modal identity.
In Marcus Kracht, Maarten de Rijke, Heinrich Wansing, and Michael
Zakharyaschev, editors, Advances in Modal Logic. Volume 1, pages
1-21. CSLI Publications, Stanford, 1998, Copyright
© 1998 CSLI.
Abstract:In this paper we describe a modal proof system arising
from the combination of a tableau-like classical system, which incorporates a
restricted (``analytical'') version of the cut rule, with a label formalism
which allows for a specialised, logic dependant unification algorithm. The
system provides a uniform proof-theoretical treatment of first-order (normal)
modal logics with identity, with and without Barcan formula and/or its
converse.
 
- Alberto Artosi, Paola Cattabriga, and Guido
Governatori.
-
An automated approach to normative
reasoning.
In Joost Breuker, editor, Artificial Normative Reasoning, pages
132-145, Amsterdam, 1994. ECAI'94.
 
- Alberto Artosi, Paola Cattabriga, and Guido
Governatori.
-
KED: A deontic theorem prover.
In Carlo Biagioli, Giovanni Sartor, and Daniela Tiscornia, editors,
Workshop on Legal Application of Logic Programming, pages 60-76,
Firenze, 1994. ICLP'94, IDG.
 
- Alberto Artosi, Paola Cattabriga, and Guido
Governatori.
-
A prolog implementation of KEM.
In Maria Alpuente and Maria I. Sessa, editors, Proceedings of
GULP-PRODE'95, pages 395-400, Salerno, 1995. Università
di Salerno.
Abstract:In this paper, we describe a Prolog implementation of a
new theorem prover for (normal propositional) modal and multi-modal logics.
The theorem prover, which is called KEM, arises from the combination of a
classical refutation system which incorporates a restricted (``analytic'')
version of the cut rule with a label formalism which allows for a specialised
logic-dependent unification algorithm. An essential feature of KEM is that
it yields a rather simple and efficient proof search procedure which offers
many computational advantages over the usual tableau-based proof search
methods. This is due partly to the use of linear 2-premise β rules in
place of the branching β rules of the standard tableau method, and
partly to the crucial role played by the analytic cut (the only branching
rule) in eliminating redundancy from the search space. It turns out that
KEM method of proof search is not only computationally more efficient but
also intuitivelly more natural than other (e.g. resolution-based) methods
leading to simple and easy implementable procedures (two KEM Theorem
Prover-like systems have been implemented: an LPA interpreter on Macintosh,
and a Quintus compiler on Sun-Sparcstation) which make it well suited for
efficient automated proof search in modal logic.
 
- Alberto Artosi, Paola Cattabriga, and Guido
Governatori.
-
A modal computational framework for default
reasoning.
In Gerhard Brewka, Christopher Habel, and Bernhard Nebel, editors,
Proceedings of KI-97, volume 1303 of LNAI, pages 373-376,
Berlin, 1997. Springer-Verlag.
 
- Alberto Artosi and Guido Governatori.
-
Labelled model modal logic.
In R. Caferra, C. Fermüller, A. Leitsch, and T. Tammet, editors,
Workshop on Automated Model Building, pages 11-17, Nancy, 1994. CADE
12.
 
- Alberto Artosi and Guido Governatori.
-
A reduplication and loop checking free proof
system for S4.
In Abstract of the 10th International Congress on Logic Methodology
and Philosophy of Science, page 43, Firenze, 1995.
 
- Alberto Artosi and Guido Governatori.
-
Modal tableaux for nonmonotonic reasoning.
In Vito Michele Abrusci, Carlo Cellucci, Roberto Cordeschi, and Vincenzo
Fano, editors, Prospettive della logica e della filosofia della
scienza, pages 203-213, Pisa, 1998. ETS.
 
- Alberto Artosi and Guido Governatori.
-
A tableaux methodology for deontic
conditional logics.
In ΔEON'98, 4th International Workshop on Deontic Logic in
Computer Science, pages 65-81, Bologna, 1998. CIRFID.
Abstract: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 possible world semantics for
conditional logics. The label formalism introduced in \cite{cade,jelia} to
account for the semantics of normal modal logics is easily adapted to the
semantics of conditional logics by simply indexing labels with formulas. The
inference rules are provided by the propositional system KE+ - a
tableau-like analytic proof system devised to be used both as a refutation
and a direct method of proof - enlarged with suitable elimination rules for
the conditional connective. The theorem proving methodology we are going to
present can be viewed as a first step towards developing an appropriate
algorithmic framework for several conditional logics for (defeasible)
conditional obligation.
 
- Alberto Artosi, Guido Governatori, and Antonino
Rotolo.
-
A labelled tableau calculus for
nonmonotonic (cumulative) consequence relations.
In Roy Dyckhoff, editor, Automated Reasoning with Analytic Tableaux and
Related Methods, volume 1847 of LNAI, pages 82-97, Berlin,
2000. Springer-Verlag, Copyright © 2000
Springer-Verlag.
Abstract:In this paper we present a labelled proof method for
computing nonmonotonic consequence relations in a conditional logic setting.
The method is based on the usual possible world semantics for conditional
logic. The label formalism KEM, introduced to account for the
semantics of normal modal logics, is easily adapted to the semantics of
conditional logic by simply indexing labels with formulas. The inference
rules are provided by the propositional system KE+ - a
tableau-like analytic proof system devised to be used both as a refutation
and a direct method of proof - enlarged with suitable elimination rules for
the conditional connective. The resulting algorithmic framework is able to
compute cumulative consequence relations in so far as they can be expressed
as conditional implications.
 
- Alberto Artosi, Guido Governatori, and Antonino
Rotolo.
-
Labelled tableaux for non-monotonic
reasoning: Cumulative consequence relations.
Journal of Logic and Computation, 12, 6, 2002.
Copyright © 2002, Oxford University Press.
Abstract:In this paper we present a labelled proof method for
computing nonmonotonic consequence relations in a conditional logic setting.
The method exploits the strong connection between these deductive relations
and conditional logics, and it is based on the usual possible world semantics
devised for the latter. The label formalism KEM, introduced to account for
the semantics of normal modal logics, is easily adapted to the semantics of
conditional logic by simply indexing labels with formulas. The basic
inference rules are provided by the propositional system KE+ - a
tableau-like analytic proof system devised to be used both as a refutation
method and a direct method of proof - that is the classical core of KEM
which is thus enlarged with suitable elimination rules for the conditional
connective. The resulting algorithmic framework is able to compute cumulative
consequence relations in so far as they can be expressed as conditional
implications.
 
- Alberto Artosi, Guido Governatori, and Giovanni
Sartor.
-
Towards a computational treatment of deontic
defeasibility.
In Mark Brown and Jos{é} Carmo, editors, Deontic Logic Agency and
Normative Systems, Workshop on Computing, pages 27-46, Berlin, 1996.
Springer-Verlag, Copyright © 1996
Springer-Verlag.
Abstract:In this paper we describe an algorithmic framework for a
multi-modal logic arising from the combination of the system of modal
(epistemic) logic devised by Meyer and van der Hoek for dealing with
nonmonotonic reasoning with a deontic logic of the Jones and Pörn-type. The
idea behind this (somewhat eclectic) formal set-up is to have a modal
framework expressive enough to model certain kinds of deontic defeasibility,
in particular by taking into account preferences on norms. The appropriate
inference mechanism is provided by a tableau-like modal theorem proving
system which supports a proof method closely related to the semantics of
modal operators. We argue that this system is particularly well-suited for
mechanizing nonmonotonic forms of inference in a monotonic multi-modal
setting.
 
- Dov M. Gabbay and Guido Governatori.
-
Dealing with label dependent deontic
modalities.
In Paul McNamara and Henry Prakken, editors, Norms, Logics and
Information Systems. New Studies in Deontic Logic, pages 311-330. IOS
Press, Amsterdam, 1998.
Abstract:In this paper, following Scott's advice, we argue that
normative reasoning can be represented in a multi-setting framework; in
particular in a multi-modal one, where modalities are indexed. Indexed
modalities can model several aspects involved in normative reasoning. Systems
are combined using Gabbay's fibring methodology which provides complete
semantics that can be used to model a labelled tableau-like proofs system.
 
- Dov M. Gabbay and Guido Governatori.
-
Fibred modal tableaux (preliminary report).
In H.M. de Swart, editor, Tableaux'98: Position Papers, Technical
Report, pages 33-48, Tilburg University, 1998.
Abstract:We describe a general and uniform tableau methodology
for multi-modal logics arising from Gabbay's methodology of fibring and
Governatori's labelled tableau system KEM.
 
- Dov M. Gabbay and Guido Governatori.
-
Fibred modal tableaux.
In David Basin, Marcello D'Agostino, Dov Gabbay, Sean Matthews, and Luca
Vigan{ó}, editors, Labelled Deduction, volume 17 of Applied
Logic Series, pages 163-194. Kluwer, Dordrecht, 2000 Copyright ©
2000, Kluwer Academic Publishers.
Abstract:We describe a general and uniform tableau methodology
for multi-modal logics arising from Gabbay's methodology of fibring and
Governatori's labelled tableau system KEM.
 
- Guido Governatori.
-
KE+: Beyond refutation.
In L. Dreschler-Fischer and S. Pribbenow, editors, KI-95 Activities:
Workshops, Posters, Demos, pages 75-76, Bonn, 1995. Gesellschaft für
Informatik.
 
- Guido Governatori.
-
Labelled tableaux for multi-modal
logics.
In P. Baumgartner, R. Hähnle, and J. Posegga, editors, Theorem
Proving with Analytic Tableaux and Related Methods, volume 918 of
LNAI, pages 79-94, Berlin, 1995. Springer-Verlag.
Abstract:In this paper we present a tableau-like proof system for
multi-modal logics based on D'Agostino and Mondadori's classical refutation
system KE. The proposed system, that we call KEM, works for the logics
S5A and S5P(n) which have been devised by Mayer and van der Hoek for
formalizing the notions of actuality and preference. We shall also show how
KEM works with the normal modal logics K45, D45, and S5 which are
frequently used as bases for epistemic operators - knowledge, belief, and we
shall briefly sketch how to combine knowledge and belief in a multi-agent
setting through KEM modularity.
 
- Guido Governatori.
-
A duplication and loop checking free system for
S4.
In D. Mundici P.Miglioli, U. Moscato and M.Ornaghi, editors, 5th
Workshop on Theorem Proving with Analytic Tableaux and Related Methods
(Short Papers), Technical Report 154-96, Università di Milano,
1996.
 
- Guido Governatori.
-
Labelling ideality and subideality.
In Dov M. Gabbay and Hans Jürgen Ohlbach, editors, Practical
Reasoning, number 1085 in LNAI, pages 291-304, Berlin, 1996.
Springer-Verlag.
Abstract:In this paper we suggest ways in which logic and law may
usefully relate; and we present an analytic proof system dealing with the
Jones Pörn's deontic logic of Ideality and Subideality, which offers some
suggestions about how to embed legal systems in label formalism.
 
- Guido Governatori.
-
Un modello formale per il ragionamento
giuridico.
PhD thesis, CIRFID, University of Bologna, Bologna, 1997.
 
- Guido Governatori.
-
Ideality and subideality from a
computational point of view.
In Alberto Artosi, Manuel Atienza, and Hajme Yoshino, editors, From
Practical Reason to Legal Computer Science. Legal Computer Science,
volume Part II, pages 315-329. Clueb, Bologna, 1998.
 
- Guido Governatori.
-
On the relative complexity of modal
tableaux.
In James Harland, editor, CATS'03, volume 78 of Electronic Notes
in Theoretical Computer Science, pages 36-53, Adelaide, 4-7 February
2003. Elsevier.
Abstract:We investigate the relative complexity of two
free-variable labelled modal tableaux (KEM and Single Step Tableaux, SST).
We discuss the reasons why p-simulation is not a proper measure of the
relative complexity of tableaux-like proof systems, and we propose an
improved comparison scale (p-search-simulation). Finally we show that KEM
p-search-simulates SST while SST cannot p-search-simulate KEM.
 
- Guido Governatori.
-
Labelled modal
tableaux.
In Carlos Areces, Patrick Blackburn, and Rob Goldblatt, editors, Advances
in Modal Logic, volume 7. College Publications, London, 2008.
Abstract: Labelled tableaux are extensions of semantic tableaux
with annotations (labels, indices) whose main function is to enrich the modal
object language with semantic elements. This paper consists of three parts.
In the first part we consider some options for labels: simple constant labels
vs labels with free variables, logic depended inference rules vs labels
manipulation based on a label algebra. In the second and third part we
concentrate on a particular labelled tableaux system called KEM using free
variable and a specialised label algebra. Specifically in the second part we
show how labelled tableaux (KEM) can account for different types of logics
(e.g., non-normal modal logics and conditional logics). In the third and
final part we investigate the relative complexity of labelled tableaux
systems and we show that the uses of KEM's label algebra can lead to speed up
on proofs.
 
- Guido Governatori, Alessio Lomuscio, and Marek
Sergot.
-
A tableaux system for deontic interpreted
systems.
In Tamás D. Gedeon and Lance Chun Che Fung, editors, AI 2003:
Advances in Artificial Intelligence, volume 2903 of LNAI, pages
339-351, Springer-Verlag, Berlin, 2003. Copyright © 2003 Springer-Verlag.
Abstract:We develop a labelled tableaux system for the modal
logic $KD45^i-j_n$ extended with epistemic notions. This logic
characterises a particular type of interpreted systems used to represent and
reason about states of correct and incorrect functioning behaviour of the
agents in a system, and of the system as a whole. The resulting tableaux
system provides a simple decision procedure for the logic. We discuss these
issues and we illustrate them with the help of simple examples.
 
- Guido Governatori and Alessandro Luppi.
-
Labelled tableaux for non-normal modal
logics.
In Evelina Lamma and Paola Mello, editors, AI*IA 99, pages 413-422,
Bologna, 1999. Pitagora.
Abstract:In this paper we show how to extend KEM, a
tableaux-like proof system for normal modal logic, in order to deal with
classes of non-normal modal logic, such as monotonic and regular, in a
uniform and modular way.
 
- Guido Governatori, Mehmet A. Orgun, and Chuchang
Liu.
-
Modal
tableaux for verifying stream authentication protocols.
Journal of Autonomous Agents and Multi Agent Systems, 19 no.
1: 53-75, 2009, Copyright © 2008
Springer.
Abstract: To develop theories to specify and reason about various
aspects of multi-agent systems, many researchers have proposed the use of
modal logics such as belief logics, logics of knowledge, and logics of norms.
As multi-agent systems operate in dynamic environments, there is also a need
to model the evolution of multi-agent systems through time. In order to
introduce a temporal dimension to a belief logic, we combine it with a
linear-time temporal logic using a powerful technique called fibring for
combining logics. We describe a labelled modal tableaux system for the
resulting fibred belief logic (FL) which can be used to automatically verify
correctness of inter-agent stream authentication protocols. With the
resulting fibred belief logic and its associated modal tableaux, one is able
to build theories of trust for the description of, and reasoning about,
multi-agent systems operating in dynamic environments.
- Guido Governatori and Antonino Rotolo.
-
Labelled modal sequents.
In Methods for Modalities 1, Amsterdam, May 6-7 1999. ILLC,
University of Amsterdam.
 
- Guido Governatori and Antonino Rotolo.
-
Labelled modal sequents.
In Roy Dyckhoff, editor, Position Papers and Tutorials, TABLEAUX
2000, Scientific Report CS/00/001, pages 3-21. School of Computer
Science, University of St Andrews, 2000.
Abstract: In this paper we present a new labelled sequent calculus
for modal logic. The proof method works with a more ``liberal'' modal
language which allows inferential steps where different formulas refer to
different labels without moving to a particular world and there computing if
the consequence holds. World-paths can be composed, decomposed and
manipulated through unification algorithms and formulas in different worlds
can be compared even if they are sub-formulas which do not depend directly on
the main connective. Accordingly, such a sequent system can provide a general
definition of modal consequence relation. Finally, we briefly sketch a proof
of the soundness and completeness results.
 
-
Mehmet A. Orgun and Guido Governatori and Chuchang Liu
-
Modal Tableaux for Verifying Security Protocols. In Dunin-Keplicz, Barbara and Verbrugge, Rineke, editors,
Formal Approaches to Multi-Agent Systems (FAMAS 2006), pages
31-46. Riva del Garda, 28-29 August, 2006.
Abstract: To develop theories to specify and reason about
various aspects of multi-agent systems, many
researchers have proposed the use of modal logics
such as belief logics, logics of knowledge, and
logics of norms. As multi-agent systems operate in
dynamic environments, there is also a need to model
the evolution of multi-agent systems through
time. In order to introduce a temporal dimension to
a belief logic, we combine it with a linear-time
temporal logic using a powerful technique called
fibring for combining logics. We describe a
labelled modal tableaux system for a fibred belief
logic (FL) which can be used to automatically verify
correctness of inter-agent stream authentication
protocols. With the resulting fibred belief logic
and its associated modal tableaux, one is able to
build theories of trust for the description of, and
reasoning about, multi-agent systems operating in
dynamic environments.
 
-
Guido Governatori and Antonino Rotolo.
-
BIO Logical Agents: Norms, Beliefs, Intentions in Defeasible Logic.
In Guido Boella, Leon van der Torre and Harko Verhagen, editors,
Normative Multi-agent Systems.
Dagstuhl Seminar Proceedings 7122.
Internationales Begegnungs- und Forschungszentrum fuer Informatik
(IBFI), Schloss Dagstuhl, Germany, Dagstuhl, Germany, 2007.
Abstract: In this paper we follow the BOID (Belief, Obligation,
Intention, Desire) architecture to describe agents and agent types in
Defeasible Logic. We argue, in particular, that the introduction of
obligations can provide a new reading of the concepts of intention and
intentionality. Then we examine the notion of social agent (i.e., an
agent where obligations prevail over intentions) and discuss some
computational and philosophical issues related to it. We show that the
notion of social agent either requires more complex computations or
has some philosophical drawbacks.
 
- Vineet Padmanabhan and Guido
Governatori.
-
On constructing fibred tableaux for BDI logics.
In Qiang Yang and Geoff Webb, editors, Ninth Pacific Rim International
Conference on Artificial Intelligence, LNAI 4099, pages
150-160, Guilin, 7-11 August 2006. Springer, Copyright © 2006 Springer.
Abstract:In [x] we showed how to combine
propositional BDI logics using Gabbay's fibring methodology. In this
paper we extend the above mentioned works by providing a tableau-based
decision procedure for the combined/fibred logics. We show how to uniformly
construct a tableau calculus for the combined logic using Governatori's
labelled tableau system KEM.