Result 1 to 20 of 33 total
Formalization of a normalization theorem in simplicial topology. (English)
Ann. Math. Artif. Intell. 64, No. 1, 1-37 (2012).
1
Proof pearl: a formal proof of Higman’s lemma in ACL2. (English)
J. Autom. Reasoning 47, No. 3, 229-250 (2011).
2
Applying ACL2 to the formalization of algebraic topology: simplicial polynomials. (English)
van Eekelen, Marko (ed.) et al., Interactive theorem proving. Second international conference, ITP 2011, Berg en Dal, The Netherlands, August 22‒25, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-22862-9/pbk). Lecture Notes in Computer Science 6898, 200-215 (2011).
3
Applying ACL2 to the formalization of algebraic topology: simplicial polynomials (English)
ITP, 200-215 (2011).
4
Simplicial topology in ACL2. (Spanish)
Lambán, Laureano (ed.) et al., Contribuciones científicas en honor de Mirian Andrés Gómez. Logroño: Universidad de La Rioja, Servicio de Publicaciones (ISBN 978-84-96487-50-5/hbk). 1-19 (2010).
5
A verified common lisp implementation of Buchberger’s algorithm in ACL2. (English)
J. Symb. Comput. 45, No. 1, 96-123 (2010).
6
ACL2 verification of simplicial degeneracy programs in the Kenzo system. (English)
Carette, Jacques (ed.) et al., Intelligent computer mathematics. 16th symposium, Calculemus 2009, 8th international conference, MKM 2009, held as part of CICM 2009, Grand Bend, Canada, July 6‒12, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-02613-3/pbk). Lecture Notes in Computer Science 5625. Lecture Notes in Artificial Intelligence, 106-121 (2009).
7
ACL2 verification of simplicial degeneracy programs in the kenzo system (English)
Calculemus/MKM, 106-121 (2009).
8
Constructing formally verified reasoners for the ACC description logic. (English)
Electron. Notes Theor. Comput. Sci. 200, No. 3, 87-102 (2008).
9
Efficient execution in an automated reasoning environment. (English)
J. Funct. Program. 18, No. 1, 15-46 (2008).
10
A formally verified prover for the $\mathcal{ALC}$ description logic. (English)
Schneider, Klaus (ed.) et al., Theorem proving in higher order logics. 20th international conference, TPHOLs 2007, Kaiserslautern, Germany, September 10‒13, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-74590-7/pbk). Lecture Notes in Computer Science 4732, 135-150 (2007).
11
A formally verified prover for the {\it ALC} description logic (English)
TPHOLs, 135-150 (2007).
12
Formal correctness of a quadratic unification algorithm. (English)
J. Autom. Reasoning 37, No. 1-2, 67-92 (2006).
13
Proof pearl: a formal proof of Higman’s Lemma in ACL2. (English)
Hurd, Joe (ed.) et al., Theorem proving in higher order logics. 18th international conference, TPHOLs 2005, Oxford, UK, August 22‒25, 2005. Proceedings. Berlin: Springer (ISBN 3-540-28372-2/pbk). Lecture Notes in Computer Science 3603, 358-372 (2005).
14
Proof pearl: A formal proof of higman’s lemma in ACL2 (English)
TPHOLs, 358-372 (2005).
15
Formal verification of a generic framework to synthesize SAT-provers. (English)
J. Autom. Reasoning 32, No. 4, 287-313 (2004).
16
Formal reasoning about efficient data structures: A case study in ACL2. (English)
Bruynooghe, Maurice (ed.), Logic based program synthesis and transformation. 13th international symposium, LOPSTR 2003, Uppsala, Sweden, August 25‒27, 2003. Revised selected papers. Berlin: Springer (ISBN 3-540-22174-3/pbk). Lecture Notes in Computer Science 3018, 75-91 (2004).
17
Verified computer algebra in ACL2 (Gröbner bases computation). (English)
Buchberger, Bruno (ed.) et al., Artificial intelligence and symbolic computation. 7th international conference, AISC 2004, Linz, Austria, September 22‒24, 2004. Proceedings. Berlin: Springer (ISBN 3-540-23212-5/pbk). Lecture Notes in Computer Science 3249. Lecture Notes in Artificial Intelligence, 171-184 (2004).
18
Verification of the formal concept analysis. (English)
RACSAM, Rev. R. Acad. Cienc. Exactas Fís. Nat., Ser. A Mat. 98, No. 1-2, 3-16 (2004).
19
Verified computer algebra in acl2. Gröbner bases computation (English)
AISC, 171-184 (2004).
20
Result 1 to 20 of 33 total