Publications

Export 11 results:
Author Title Type [ Year(Asc)]
Filters: Author is Alonso-Jiménez, J.A.  [Clear All Filters]
2002
I. Medina-Bulo, Alonso-Jimenez, J. A., and Palomo-Lozano, F., Algoritmos polinómicos en ACL2 (una aproximación al algoritmo de Buchberger), I Taller Iberoamericano sobre Deducción Automática e Inteligencia Artificial (Conferencia Iberoamericana de Inteligencia artificial). Sevilla, Spain, 2002.
I. Medina-Bulo, Palomo-Lozano, F., and Alonso-Jimenez, J. A., Implementation in Acl2 of Well-Founded Polynomial Orderings, The European Joint Conferences on Theory and Practice of Software (ETAPS). Grenoble (France), pp. 66-67, 2002.
2001
I. Medina-Bulo, Palomo-Lozano, F., and Alonso-Jiménez, J. A., Certification of matrix multiplication algorithms. Strassen's algorithm in ACL2,, 14th International Conference on Theorem Proving in Higher Order Logics. Division of Informatics, Edinburgh (Scotland), pp. 283-298, 2001.
I. Medina-Bulo, Palomo-Lozano, F., and Alonso-Jiménez, J. A., A certified algorithm for translating formulas into polynomials. An ACL2 approach, International Joint Conference on Automated Reasoning (CADE + FTP + TABLEAUX) , Siena (Italy). 2001.
I. Medina-Bulo, Palomo-Lozano, F., and Alonso-Jiménez, J. A., A certified polynomial-based decision procedure for propositional logic, Proceedings of the 14th International Conference on Theorem Proving in Higher Order Logics (TPHOL 2001), Edinburgh (Scotland), vol. LNCS 2152. pp. 297-312, 2001.
I. Medina-Bulo, Palomo-Lozano, F., and Alonso-Jiménez, J. - A., A certified polynomial-based decision procedure for propositional logic, Lecture Notes in Computer Science, vol. 2152, p. 312, 2001.
2000
I. Medina-Bulo, Palomo-Lozano, F., and Alonso-Jiménez, J. A., Automatic verification of polynomial rings fundamental properties in ACL2,, ACL2 Workshop 2000 Proceedings, vol. Part A. Universidad de Texas, Department of Computer Sciences. Technical Report TR--00--29, Austin (USA), pp. 136-155, 2000.
F. Palomo-Lozano, Alonso-Jiménez, J. A., and Medina-Bulo, I., Reasoning about matrix arithmetic in ACL2, Workshop AOC. Lyon (France), 2000.