Last modified: Wed Apr 21 07:30:20 -05 2021
Combining Interactive and Automatic Proofs in
First-Order Theories
Andrés Sicard-Ramírez and
Juan-Fernando Ospina-Giraldo
Universidad EAFIT. Grant:
7. 2014. Work in progress.
Abstract: In Bove, Dybjer and Sicard-Ramírez (2012), ‘Combining Interactive and Automatic Reasoning in First Order Theories of Functional Programs’, LNCS 7213, we proposed a first-order theory—the First Order Theory of Combinators (FOTC)—for reasoning about functional programs by combining interactive proofs performed in the Agda proof assistant and automatic proofs performed by off-the-shelf automatic theorem provers for first-order logic (ATPs). Our approach can be used with other first-order theories too. We have used it not only for FOTC, but also for other first-order theories such as Group Theory and Peano Arithmetic, and we had encouraging results. We propose extending the automatic proof capabilities of our approach by using, in addition to the ATPs, Satisfiability Modulo Theories solvers.
Hipercomputación desde la computación cuántica
(Hypercomputation based on quantum computation)
Andrés Sicard Ramírez, Mario Elkin Vélez Ruiz and Juan
Fernando Ospina Giraldo
Universidad
EAFIT–COLCIENCIAS. Grant: 1216-05-13576. 2004. [ pdf
]
Computación cuántica geométrica no abeliana
(Non-abelian geometric quantum computation)
Mario
Elkin Vélez Ruiz and Andrés Sicard Ramírez
Universidad
EAFIT. Grant: PY0017. 2002. [ tar.gz ]
Computación paraconsistente (Paraconsistent
computation)
Andrés Sicard Ramírez
Universidad EAFIT. Grant: PY0084. 2001 [ pdf ]
Computación cuántica geométrica (Geometric quantum
computation)
Mario Elkin Vélez Ruiz and Andrés
Sicard Ramírez
Universidad EAFIT. Grant:
817431. 2001. [ tar.gz
]
Prototipo de un modelo de computación cuántica
continua (A continuous quantum computation model)
Andrés Sicard Ramírez and Mario Elkin Vélez Ruiz
Universidad EAFIT. Grant: 817424. 2000. [ tar.gz ]
¿Máquina de Turing cuántica autorrefencial: Una
posibilidad? (Self-referential quantum Turing machine)
Andrés Sicard Ramírez and Mario Elkin Vélez Ruiz
Universidad EAFIT. Grant: 817407. 1999. [ tar.gz ]
Lenguaje subyacente a la noción de máquina cuántica
(Underline language for quantum computation)
Andrés
Sicard Ramírez, María Eugenia Puerta Yepes and Mario Elkin Vélez
Ruiz
Universidad EAFIT. Grant: 817405. 1998. [ pdf ]
Máquinas de Turing dinámicas: Historia y desarrollo de
una idea (Dynamic Turing machines)
Andrés Sicard
Ramírez
Universidad EAFIT. Grant: PY0084. 1997. [ pdf ]
| Andrés
Sicard Ramírez
Last modified: Wed Apr 21 07:30:20 -05 2021 |