Name
Abstract | ||
|---|---|---|
This paper presents a resolution decision procedure for tran- sitive propositional modal logics. The procedure combines the relational translation method with an ordered chaining calculus designed to avoid unnecessary inferences with transitive relations. We show the logics K4, KD4 and S4 can be transformed into a bounded class of well-structured clauses closed under ordered resolution and negative chaining. Area: Computational aspects of modal logic |
Year | Venue | Keywords |
|---|---|---|
1998 | Advances in Modal Logic 2006 | modal logic |
Field | DocType | Citations |
Decision tree,Chaining,Computer science,Algorithm,Theoretical computer science,Modal logic,Modal,Bounded function,Transitive relation | Conference | 15 |
PageRank | References | Authors |
0.95 | 10 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Harald Ganzinger | 1 | 1513 | 155.21 |
| Ullrich Hustadt | 2 | 1007 | 66.68 |
| Christoph Meyer | 3 | 17 | 2.17 |
| Renate A. Schmidt | 4 | 857 | 83.52 |