| Publication | Date of Publication | Type |
|---|
| Using abstract stobjs in ACL2 to compute matrix normal forms | 2018-01-04 | Paper |
Certified symbolic manipulation: bivariate simplicial polynomials
Proceedings of the 38th International Symposium on Symbolic and Algebraic Computation | 2017-02-10 | Paper |
Formally verified tableau-based reasoners for a description logic
Journal of Automated Reasoning | 2015-06-23 | Paper |
Modelling algebraic structures and morphisms in ACL2
Applicable Algebra in Engineering, Communication and Computing | 2015-06-22 | Paper |
Verifying the bridge between simplicial topology and algebra: the Eilenberg-Zilber algorithm
Logic Journal of the IGPL | 2015-02-12 | Paper |
Formalization of a normalization theorem in simplicial topology
Annals of Mathematics and Artificial Intelligence | 2012-12-28 | Paper |
Proof pearl: a formal proof of Higman's lemma in ACL2
Journal of Automated Reasoning | 2012-07-31 | Paper |
Applying ACL2 to the formalization of algebraic topology: simplicial polynomials
Interactive Theorem Proving | 2011-08-17 | Paper |
Verification in ACL2 of a generic framework to synthesize SAT-provers
Logic Based Program Synthesis and Transformation | 2011-03-04 | Paper |
| Simplicial topology in ACL2 | 2011-01-03 | Paper |
| A formal proof of Dickson's lemma in ACL2 | 2010-02-24 | Paper |
ACL2 Verification of Simplicial Degeneracy Programs in the Kenzo System
Lecture Notes in Computer Science | 2009-07-09 | Paper |
A Formally Verified Prover for the $\mathcal{ALC\,}$ Description Logic
Lecture Notes in Computer Science | 2008-09-02 | Paper |
Formal correctness of a quadratic unification algorithm
Journal of Automated Reasoning | 2007-05-03 | Paper |
Computer Aided Systems Theory – EUROCAST 2005
Lecture Notes in Computer Science | 2006-11-01 | Paper |
Theorem Proving in Higher Order Logics
Lecture Notes in Computer Science | 2006-07-06 | Paper |
Formal verification of a generic framework to synthesize SAT-provers
Journal of Automated Reasoning | 2006-01-16 | Paper |
Logic Based Program Synthesis and Transformation
Lecture Notes in Computer Science | 2005-12-27 | Paper |
| scientific article; zbMATH DE number 2177622 (Why is no real title available?) | 2005-06-21 | Paper |
| scientific article; zbMATH DE number 2154398 (Why is no real title available?) | 2005-04-09 | Paper |
| scientific article; zbMATH DE number 2079835 (Why is no real title available?) | 2004-07-30 | Paper |
| scientific article; zbMATH DE number 2013803 (Why is no real title available?) | 2003-12-07 | Paper |
| scientific article; zbMATH DE number 2000443 (Why is no real title available?) | 2003-11-03 | Paper |
Formal proofs about rewriting using ACL2
Annals of Mathematics and Artificial Intelligence | 2002-08-19 | Paper |
