Diferencia entre revisiones de «Theories»

De WikiGLC
Saltar a: navegación, buscar
Línea 2: Línea 2:
 
* [[A Formalization of Abstract Properties of Confluent Reductions in PVS]].
 
* [[A Formalization of Abstract Properties of Confluent Reductions in PVS]].
 
* [[Proving termination with multiset orderings in PVS: theory, methodology and applications (PROTEMO)]].
 
* [[Proving termination with multiset orderings in PVS: theory, methodology and applications (PROTEMO)]].
 +
* [[A formally verified prover for the ALC description logic (or Constructing formally verified reasoners for the ALC description logic)]].
 +
* [[Verification of the formal concept analysis in PVS]].
 +
* [[A formally verified proof in PVS of the strong completeness theorem of propositional SLD-resolution]].
 +
* [[Refinements]].
 
* [http://www.cs.us.es/~jalonso/trabajos_dirigidos/Teoria_computacional_en_ACL2_sobre_calculos_proposicionales.zip Teoría computacional (en ACL2) sobre cálculos proposicionales].
 
* [http://www.cs.us.es/~jalonso/trabajos_dirigidos/Teoria_computacional_en_ACL2_sobre_calculos_proposicionales.zip Teoría computacional (en ACL2) sobre cálculos proposicionales].
 
* [http://www.cs.us.es/~jruiz/acl2-rewr/ Formalizing equational reasoning and rewriting (using ACL2)]
 
* [http://www.cs.us.es/~jruiz/acl2-rewr/ Formalizing equational reasoning and rewriting (using ACL2)]

Revisión del 18:32 1 jun 2010