ISSN:
1573-0670
Keywords:
modal logic
;
translation methods
;
set theory
;
theorem proving
Source:
Springer Online Journal Archives 1860-2000
Topics:
Computer Science
Notes:
Abstract The paper presents aset-theoretic translation method for polymodal logics that reduces derivability in a large class of propositional polymodal logics to derivability in a very weak first-order set theory Ω. Unlike most existing translation methods, the one we propose applies to any normal complete finitely axiomatizable polymodal logic, regardless of whether it is first-order complete or an explicit semantics is available. The finite axiomatizability of Ω allows one to implement mechanical proof-search procedures via the deduction theorem. Alternatively, more specialized and efficient techniques can be employed. In the last part of the paper, we briefly discuss the application ofset T-resolution to support automated derivability in (a suitable extension of) Ω.
Type of Medium:
Electronic Resource
URL:
http://dx.doi.org/10.1007/BF00881803
Permalink
