A resolution prover for coalition logic

C. Nalon; L. Zhang; C. Dixon; U. Hustadt

doi:10.4204/EPTCS.146.9

A resolution prover for coalition logic

C. Nalon, L. Zhang, C. Dixon, U. Hustadt

Formal Methods

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

Abstract

We present a prototype tool for automated reasoning for Coalition Logic, a non-normal modal logic that can be used for reasoning about cooperative agency. The theorem prover CLProver is based on recent work on a resolution-based calculus for Coalition Logic that operates on coalition problems, a normal form for Coalition Logic. We provide an overview of coalition problems and of the resolutionbased calculus for Coalition Logic. We then give details of the implementation of CLProver and present the results for a comparison with an existing tableau-based solver.

Original language	English
Title of host publication	Electronic Proceedings in Theoretical Computer Science (EPTCS)
Pages	65-73
Number of pages	9
Volume	146
DOIs	https://doi.org/10.4204/EPTCS.146.9
Publication status	Published - 1 Apr 2014
Event	2nd International Workshop on Strategic Reasoning - Grenoble, France Duration: 5 Apr 2014 → 6 Apr 2014 Conference number: 113242

Conference

Conference	2nd International Workshop on Strategic Reasoning
Abbreviated title	SR 2014
Country/Territory	France
City	Grenoble
Period	5/04/14 → 6/04/14

Access to Document

10.4204/EPTCS.146.9

Cite this

@inproceedings{8a79b84b5ed5497d97ecd950c37b31cc,

title = "A resolution prover for coalition logic",

abstract = "We present a prototype tool for automated reasoning for Coalition Logic, a non-normal modal logic that can be used for reasoning about cooperative agency. The theorem prover CLProver is based on recent work on a resolution-based calculus for Coalition Logic that operates on coalition problems, a normal form for Coalition Logic. We provide an overview of coalition problems and of the resolutionbased calculus for Coalition Logic. We then give details of the implementation of CLProver and present the results for a comparison with an existing tableau-based solver.",

author = "C. Nalon and L. Zhang and C. Dixon and U. Hustadt",

year = "2014",

month = apr,

day = "1",

doi = "10.4204/EPTCS.146.9",

language = "English",

volume = "146",

pages = "65--73",

booktitle = "Electronic Proceedings in Theoretical Computer Science (EPTCS)",

note = "2nd International Workshop on Strategic Reasoning, SR 2014 ; Conference date: 05-04-2014 Through 06-04-2014",

}

TY - GEN

T1 - A resolution prover for coalition logic

AU - Nalon, C.

AU - Zhang, L.

AU - Dixon, C.

AU - Hustadt, U.

N1 - Conference code: 113242

PY - 2014/4/1

Y1 - 2014/4/1

N2 - We present a prototype tool for automated reasoning for Coalition Logic, a non-normal modal logic that can be used for reasoning about cooperative agency. The theorem prover CLProver is based on recent work on a resolution-based calculus for Coalition Logic that operates on coalition problems, a normal form for Coalition Logic. We provide an overview of coalition problems and of the resolutionbased calculus for Coalition Logic. We then give details of the implementation of CLProver and present the results for a comparison with an existing tableau-based solver.

AB - We present a prototype tool for automated reasoning for Coalition Logic, a non-normal modal logic that can be used for reasoning about cooperative agency. The theorem prover CLProver is based on recent work on a resolution-based calculus for Coalition Logic that operates on coalition problems, a normal form for Coalition Logic. We provide an overview of coalition problems and of the resolutionbased calculus for Coalition Logic. We then give details of the implementation of CLProver and present the results for a comparison with an existing tableau-based solver.

UR - http://www.scopus.com/inward/record.url?eid=2-s2.0-84938564369&partnerID=MN8TOARS

U2 - 10.4204/EPTCS.146.9

DO - 10.4204/EPTCS.146.9

M3 - Conference contribution

VL - 146

SP - 65

EP - 73

BT - Electronic Proceedings in Theoretical Computer Science (EPTCS)

T2 - 2nd International Workshop on Strategic Reasoning

Y2 - 5 April 2014 through 6 April 2014

ER -

A resolution prover for coalition logic

Abstract

Conference

Access to Document

Other files and links

Fingerprint

Cite this