-
Notifications
You must be signed in to change notification settings - Fork 1
/
abstract.tex
20 lines (18 loc) · 1.14 KB
/
abstract.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
\pdfbookmark[1]{Abstract}{Abstract}
%\addcontentsline{toc}{chapter}{\tocEntry{Abstract}}
\begingroup
\let\clearpage\relax
\let\cleardoublepage\relax
\let\cleardoublepage\relax
\chapter*{Abstract}
First-Order Linear Temporal Logic (FOLTL) is the extension of the well-known propositional Linear Temporal Logic with
first-order quantification. Its interpretation is classically over \emph{Kripke-frames}, that is, a set of time-points
or worlds and an accessibility relation, the properties of which determine the axioms of the logic. However, such
interpretation suffers limitations, since it requires restrictions on the accessibility relation between worlds. We
introduce a novel semantics for FOLTL based on \emph{counterpart relations}, i.e. families of partial homomorphisms
between algebras. This approach overcomes most limitations, completely removing the \emph{trans-world identity problem}
and thus streamlining the modeling of dynamic creation, deletion and merging of entities. We also provide the logic with
a Hilbert-style deductive system, and we conclude with consideration about completeness, decidability and possible
extensions.
\endgroup
\vfill