Diferencia entre revisiones de «Theories»

De WikiGLC
Saltar a: navegación, buscar
(Resources)
Línea 1: Línea 1:
 
== Theories ==
 
== Theories ==
 +
=== Theories in PVS ===
 
# [[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)]].
Línea 6: Línea 7:
 
# [[A formally verified proof in PVS of the strong completeness theorem of propositional SLD-resolution]].
 
# [[A formally verified proof in PVS of the strong completeness theorem of propositional SLD-resolution]].
 
# [[Theory of Refinements in PVS]].
 
# [[Theory of Refinements in PVS]].
 +
=== Theories in ACL2 ===
 
# [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)]
Línea 13: Línea 15:
 
# [http://www.cs.us.es/~fmartin/acl2/gen-sat/ A generic framework for propositional SAT-provers (formalization in ACL2)]
 
# [http://www.cs.us.es/~fmartin/acl2/gen-sat/ A generic framework for propositional SAT-provers (formalization in ACL2)]
 
# [http://www.cs.us.es/~fmartin/acl2/dickson/ Formalization and proof of Dickson's Lemma in ACL2]
 
# [http://www.cs.us.es/~fmartin/acl2/dickson/ Formalization and proof of Dickson's Lemma in ACL2]
 +
=== Theories in Haskell/QuickCheck ===
 
# [http://www.glc.us.es/theories/deltarule/CLAI2009.hs Haskell implementation of Independence Rule]
 
# [http://www.glc.us.es/theories/deltarule/CLAI2009.hs Haskell implementation of Independence Rule]
  

Revisión del 12:44 7 jul 2010