Nalon, Cláudia, Zhang, Lan, Dixon, Clare 
ORCID: 0000-0002-4610-9533 and Hustadt, Ullrich ORCID: 0000-0002-0455-0267
(2014)
A Resolution Prover for Coalition Logic.
.
![[img]](https://livrepository.liverpool.ac.uk/style/images/fileicons/text.png) |
Text
SR2014.9.pdf - OA Published Version Download (492kB) |
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 resolution-based 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.
| Item Type: | Conference or Workshop Item (Unspecified) |
|---|---|
| Additional Information: | In Proceedings SR 2014, arXiv:1404.0414 |
| Uncontrolled Keywords: | cs.LO, cs.LO, cs.AI, I.2.3;F.4.1 |
| Depositing User: | Symplectic Admin |
| Date Deposited: | 06 Jul 2017 13:07 |
| Last Modified: | 04 Aug 2022 07:10 |
| Related URLs: | |
| URI: | https://livrepository.liverpool.ac.uk/id/eprint/3008348 |
Share
Share
