|
Zapiski Nauchnykh Seminarov POMI, 1995, Volume 220, Pages 123–144
(Mi znsl4284)
|
|
|
|
Saturated calculus for Horn-like sequents of a complete class of a linear temporal first order logic
Regimantas Pliuškevičius Institute of Mathematics and Informatics, Vilnius
Abstract:
A saturated calculus for the so-called Horn-like sequents of a complete class of a linear temporal logic of the first order is described. The saturated calculus contains neither induction-like postulates nor cut-like rules. Instead of induction-like postulates the saturated calculus contains a finite set of “saturated” sequents, which (1) capture and reflect the periodic structure of inductive reasoning (i.e., a reasoning which applies inductionlike postulates); (2) show that “almost nothing new” can be obtained by continuing the process of derivation of a given sequent; (3) present an explicit way of generating the so-called invariant formula in induction-like rules. The saturated calculus for Horn-like sequents allows one: (1) to prove in an obvious way the completeness of a restricted linear temporal logic of the first order; (2) to construct a computer-aided proof system for this logic; (3) to prove the decidability of this logic for logically decidable Horn-like sequents. Bibliography: 15 titles.
Received: 20.06.1994
Citation:
Regimantas Pliuškevičius, “Saturated calculus for Horn-like sequents of a complete class of a linear temporal first order logic”, Studies in constructive mathematics and mathematical logic. Part IX, Zap. Nauchn. Sem. POMI, 220, POMI, St. Petersburg, 1995, 123–144; J. Math. Sci. (New York), 87:1 (1997), 3253–3266
Linking options:
https://www.mathnet.ru/eng/znsl4284 https://www.mathnet.ru/eng/znsl/v220/p123
|
Statistics & downloads: |
Abstract page: | 117 | Full-text PDF : | 56 |
|