A strongly complete proof system for propositional dynamic logic

Gerard Renardel de Lavalette; Barteld Kooi; Rineke Verbrugge

A strongly complete proof system for propositional dynamic logic

Gerard Renardel de Lavalette, Barteld Kooi, Rineke Verbrugge

Research output: Chapter in Book/Report/Conference proceeding › Chapter › Academic

Abstract

Propositional dynamic logic (PDL) is complete but not compact. As a consequence, strong completeness (the property Γ |= φ ⇒ Γ |- φ) does not hold for the standard finitary axiomatisation. In this paper, we present an infinitary proof system of PDL and prove strong completeness. The result is extended to epistemic logic with common knowledge.

Original language	English
Title of host publication	Institut de Recherche en Informatique de Toulouse IRIT (2002)
Publisher	University of Groningen, Johann Bernoulli Institute for Mathematics and Computer Science
Pages	377-393
Number of pages	17
Publication status	Published - 2002

Handle.net

Persistent link

Embargoed Document

2002ProcAiMLRenardeldeL2.pdf
Final publisher's version, 238 KB
Request copy

Cite this

@inbook{0e049f98c0b646e38530e3b7b3625391,

title = "A strongly complete proof system for propositional dynamic logic",

abstract = "Propositional dynamic logic (PDL) is complete but not compact. As a consequence, strong completeness (the property Γ |= φ ⇒ Γ |- φ) does not hold for the standard finitary axiomatisation. In this paper, we present an infinitary proof system of PDL and prove strong completeness. The result is extended to epistemic logic with common knowledge.",

author = "{Renardel de Lavalette}, Gerard and Barteld Kooi and Rineke Verbrugge",

note = "Relation: http://www.rug.nl/informatica/organisatie/overorganisatie/iwi Rights: University of Groningen. Research Institute for Mathematics and Computing Science (IWI)",

year = "2002",

language = "English",

pages = "377--393",

booktitle = "Institut de Recherche en Informatique de Toulouse IRIT (2002)",

publisher = "University of Groningen, Johann Bernoulli Institute for Mathematics and Computer Science",

}

A strongly complete proof system for propositional dynamic logic. / Renardel de Lavalette, Gerard ; Kooi, Barteld ; Verbrugge, Rineke.
Institut de Recherche en Informatique de Toulouse IRIT (2002) . University of Groningen, Johann Bernoulli Institute for Mathematics and Computer Science, 2002. p. 377-393.

Research output: Chapter in Book/Report/Conference proceeding › Chapter › Academic

TY - CHAP

T1 - A strongly complete proof system for propositional dynamic logic

AU - Renardel de Lavalette, Gerard

AU - Kooi, Barteld

AU - Verbrugge, Rineke

N1 - Relation: http://www.rug.nl/informatica/organisatie/overorganisatie/iwi Rights: University of Groningen. Research Institute for Mathematics and Computing Science (IWI)

PY - 2002

Y1 - 2002

N2 - Propositional dynamic logic (PDL) is complete but not compact. As a consequence, strong completeness (the property Γ |= φ ⇒ Γ |- φ) does not hold for the standard finitary axiomatisation. In this paper, we present an infinitary proof system of PDL and prove strong completeness. The result is extended to epistemic logic with common knowledge.

AB - Propositional dynamic logic (PDL) is complete but not compact. As a consequence, strong completeness (the property Γ |= φ ⇒ Γ |- φ) does not hold for the standard finitary axiomatisation. In this paper, we present an infinitary proof system of PDL and prove strong completeness. The result is extended to epistemic logic with common knowledge.

M3 - Chapter

SP - 377

EP - 393

BT - Institut de Recherche en Informatique de Toulouse IRIT (2002)

PB - University of Groningen, Johann Bernoulli Institute for Mathematics and Computer Science

ER -

A strongly complete proof system for propositional dynamic logic

Abstract

Handle.net

Embargoed Document

Fingerprint

Cite this