Loading...
Please wait, while we are loading the content...
Similar Documents
Unification and Inference Rules in the Multi-modal Logic of Knowledge and Linear Time LTK
| Content Provider | Semantic Scholar |
|---|---|
| Author | Bashmakov, Stepan I. |
| Copyright Year | 2016 |
| Abstract | The research of unification for various logic systems is one of the most rapidly developing areas of modern mathematical logic. Arisen in the field of Computer Science, primarily in the form of a question about the possibility to transform two different terms in syntactically equivalent by replacing the variables of certain other terms ( [1,2]), from the time the task has changed course on the study of semantic equivalence ( [3, 4]). For most of the non-classical logics (modal, pseudo-boolean, temporal, etc.), there are special dual equational theories of special algebraic systems, so their problems are reduced to the corresponding logical-unificational counterparts ( [5–7]). Basic unificational problem can be viewed as a complex issue: whether the formula is to be transformed into a theorem after replacing the variables (keeping the same values of the coefficients parameters). This issue was investigated and partly resolved (including V. V. Rybakov [8–10]), for intuitionistic and modal logics S4 and Grz. Unification in intuitionistic logic and in propositional modal logic over the K4 investigated by S.Ghilardi [11–15] (with applications of projective algebra ideas and technology based on projective formulas). In these works the problem of constructing the finite complete sets of unifiers was solved for the considered logic, efficient algorithms were found. Such an approach proved to be a a useful and effective in dealing with the admissibility and the basis of admissible rules (Jerabek [16–18], Iemhoff, Metcalfe [19,20]). Indeed, the existence of computable finite sets of unifiers follows directly solution of the admissibility problem. Temporal logic is also very dynamic area of mathematical logic and computer science (including Gabbay и Hodkinson [21–23]). In particular, LTL (linear temporal logic) has a significant application in the field of Computer Science (Manna, Pnueli [24,25], Vardi [26,27]). Solving the problem of admissibility of rules in the LTL was proposed by Rybakov [28], basis of admissible |
| Starting Page | 149 |
| Ending Page | 157 |
| Page Count | 9 |
| File Format | PDF HTM / HTML |
| DOI | 10.17516/1997-1397-2016-9-2-149-157 |
| Volume Number | 9 |
| Alternate Webpage(s) | http://elib.sfu-kras.ru/bitstream/handle/2311/20238/bashmakov.pdf?isAllowed=y&sequence=4 |
| Alternate Webpage(s) | https://doi.org/10.17516/1997-1397-2016-9-2-149-157 |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
