Ordered Resolution for Coalition Logic

DOI10.1007/978-3-319-24312-2_12zbMath1464.03007OpenAlexW2242222976MaRDI QIDQ3455769

Cláudia Nalon, Clare Dixon, Ullrich Hustadt, Lan Zhang, Paul Gainer

Publication date: 11 December 2015

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-24312-2_12

Mathematics Subject Classification ID

Cooperative games (91A12) Applications of game theory (91A80) Modal logic (including the logic of norms) (03B45) Logic in artificial intelligence (68T27) Mechanization of proofs and logical operations (03B35) Agent technology and artificial intelligence (68T42) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Uses Software

• VAMPIRE
• SPASS
• TATL
• TRP++
• CLProver

Cites Work

• Unnamed Item
• A structure-preserving clause form translation
• Complete axiomatization and decidability of alternating-time temporal logic
• Resolution with order and selection for hybrid logics
• TATL: Implementation of ATL Tableau-Based Decision Procedure
• System Description: E 1.8
• A resolution-based calculus for Coalition Logic
• Tableau-based decision procedures for logics of strategic ability in multiagent systems
• ATL Satisfiability is Indeed EXPTIME-complete
• Alternating-time temporal logic
• Simple and Efficient Clause Subsumption with Feature Vector Indexing
• A resolution calculus for the branching-time temporal logic CTL