Razonamiento temporal deductivo con limitaciones
Combinación de logica temporal y tiempo lineal preposicional estandar con restricciones y cardinalidad al limitar el número de literales que se pueden satisfacer en cualquier momento en el timpo
Costeñido de la
lógica temporal
(TLC)
Restringe el número de literales
que pueden ser satisfechos en
cualquier momento del tiempo
Es decir:
C ^ a m, donde a ∈ {=, ≤} y m ∈ n
La función de x se restringe m, ya que son
literales de conjunto C
(a es =) y en los literales de conjunto se cumplen
todos los estados = (a es ≤)
Se puede expresar como:
C ≤ m - 1, cuando es mayor o igual a C ≥ m
Para hallarlas, esisten dos formulas:
* ((P ∨ Q) ∧ (P ∨ R) ∧ (Q ∨ R))
* (~P ∧ ~Q ∧ ~R)
Sintaxis (TLC)
En el tiempo futuro se incluyen conectivos
temporales, como :
Y = En el momento siguiente
T = Hasta
A partir de:
* Consecutivo proposicional = "Cierto", ∧,, Y
* Consecutiva temporal = "O", "T"
Escribimos TLC (C), donde C = {C_1 ^am...C_n ^am},
se conoce como conjunto de formulas (WFF)
Es el conjunto mas pequeño donde ningun
elemento de LOS APOYO y LA VERDAD en WFF
si φ y ψ, son WFF entonces tambien lo son ~ψ, φ,
˄ψ, Oφ, φ u ψ.
Semantica (TLC)
La notación de L. L= PL φ denotan la verdad
del la lógica preposicional formula φ con
respecto al conjunto L. Donde L = pl.P ↔ P ϵ Props
y la semántica de los operadores ~, ˄ se de
costumbre; L es el conjunto de preposiciones
y C ^ am, es una restricción
Tenemos que:
Eval (L, c ^(∞m)) = {P/ P ϵ L y P ϵ C} u {~P/ P ∉ L y ~P ∉ C}
Entonces:
L = pl C^(=m) IFF / Eval (L,C ^ (= m)) / = m
L = pl C^(≤ m) IFF / Eval (L,C ^ (≤ m)) / ≤ m
Teniendo en cuenta que el operador L= pl. Solo esta definido para las fórmulas de lógica preposicional. Un conjunto C de restricción es satisfacible si y solo si existe un conjunto de proposiciones L de manera que C_1 ^ (∞m) ϵ C(¡ϵ N), L=pl C_¡ ^(∞m)
Modelo (TLC)
Para el TIC (c) las formas se pueden caracterizar como una “secuencia de estados”, o de la forma O= S₁, S₂, S₃…,
donde los estados “S” son un conjunto de símbolos
que representan proposiciones satisfechos en cada
momento del tiempo. Donde “S” de satisfacer el conjunto
de restricciones C, es decir para todos S tenemos S= pl C₀.
La notación (o,i)= φ denota la verdad de la formula φ en el modelo o en el estado de indice (i ϵ N)
Se define como;
(o,i)=true
(o,i)= p iff p ϵ S₁, donde p ϵ Props
(o,i)=~φ iff este no es el caso que (o,i)= φ
(o,i)= φ^ ψ iff (o,i)= φ y (o,i)= ψ
(o,i)=O φ iff (o,i+1)= φ
(o,i)= φUψ iff ∃k ϵ N.k ≥ i y (o,k)=ψ y ∀j ϵ N, si i ≤ j< tambien
(o,i)=φ
Forma Normal
En la forma normal se introduce un ULTERIOR (nularia)
conjunto (inicio) que mantiene solo el principio de los tiempos
Es decir:
(o,i) | = star iff i=0
Pequeñas letras “K-L-J-M” represente literales PUNTUALES donde i,j ≥ 0, teniendo en cuenta la lado izquierdo si i=o y por el lado derecho si j=0. Por ende, el lado izquierdo es una conjunción cierta y el lado derecho una disyunción falsa
Las clausulas definidas se conocen como INCONDICIONALES y en SFN se define como CONDICINAL ˄ki = >Δm. Tambien podemos reescribir una clausula de algun momento incondicional usando una nueva variable “w_m” de esta manera informal se denota la ESPERA M