Oi Elaine,
do modo (torto? 8-)) como eu entendo cálculo de sequentes a sua
derivação para o "subst"
Pabb'|-Qabb'
============subst
Pabb|-Qabb
acaba envolvendo uma hipótese extra, b=b', que nunca é descartada...
Mas acabei de encontrar uma solução, ó:
[Pabb']^1
:
Qabb'
-----------1
Pabb'->Qabb'
-----------------------
b \forall b'.Pabb'->Qabb'
-----------------------------
Pabb->Qabb
que em cálculo de seqüentes "com as variáveis livres listadas antes do
ponto-e-vírgula" vira:
a,b,b';Pabb'|-Qabb'
----------------------
a,b,b';T|-Pabb'->Qabb'
------------------------------
a,b|-b a,b;T|-\forall b'.Pabb'->Qabb'
----------------------------------------
a,b;T|-Pabb->Qabb
-----------------
a,b;Pabb|-Qabb
ou seja, em sistemas com "\forall" e "->" esse tipo de substituição pode
ser visto como regra derivada...
Obrigado, [[]]s,
Eduardo Ochs
[email protected]
http://angg.twu.net/
P.S.: desculpe a demora em responder!... 8-)
_______________________________________________
Logica-l mailing list
[email protected]
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
