Solving the $100 modal logic challenge |
| |
Authors: | Florian Rabe Petr Pudlák Geoff Sutcliffe Weina Shen |
| |
Affiliation: | 1. Department of Computer Science, Carnegie Mellon University, USA;2. Department of Theoretical Computer Science and Mathematical Logic, Charles University, Czech Republic;3. Department of Computer Science, University of Miami, USA |
| |
Abstract: | We present the theoretical foundation, design, and implementation, of a system that automatically determines the subset relation between two given axiomatizations of propositional modal logics. This is an open problem for automated theorem proving. Our system solves all but six out of 121 instances formed from 11 common axiomatizations of seven modal logics. Thus, although the problem is undecidable in general, our approach is empirically successful in practically relevant situations. |
| |
Keywords: | |
本文献已被 ScienceDirect 等数据库收录! |
|