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

Onderzoeksoutput: Chapter › Academic

Samenvatting

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.

Originele taal-2	English
Titel	Institut de Recherche en Informatique de Toulouse IRIT (2002)
Uitgeverij	University of Groningen, Johann Bernoulli Institute for Mathematics and Computer Science
Pagina's	377-393
Aantal pagina's	17
Status	Published - 2002

Handle.net

Permanente koppeling

Document onder embargo

2002ProcAiMLRenardeldeL2.pdf
Final publisher's version, 238 KB
Kopie aanvragen

Citeer dit

@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",

}

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

Samenvatting

Handle.net

Document onder embargo

Vingerafdruk

Citeer dit