Executing in Common Lisp, Proving in ACL2

DOI10.1007/978-3-540-73086-6_1zbMath1202.68369OpenAlexW1496793133MaRDI QIDQ5428255

Mirian Andrés, Laureano Lambán, Julio Jesús Rubio García

Publication date: 28 November 2007

Published in: Towards Mechanized Mathematical Assistants (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-73086-6_1

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Software, source code, etc. for problems pertaining to algebraic topology (55-04)

Related Items (3)

A case-study in algebraic manipulation using mechanized reasoning tools ⋮ ACL2 Verification of Simplicial Degeneracy Programs in the Kenzo System ⋮ Formalizing in Coq Hidden Algebras to Specify Symbolic Computation Systems

Uses Software

• ACL2
• EAT

This page was built for publication: Executing in Common Lisp, Proving in ACL2