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.