Autarkic computations in formal proofs
From MaRDI portal
Publication:1610674
DOI10.1023/A:1015761529444zbMath1002.68156MaRDI QIDQ1610674
H. P. Barendregt, Erik Barendsen
Publication date: 20 August 2002
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
68W30: Symbolic computation and algebraic computation
03B35: Mechanization of proofs and logical operations
Related Items
Proof by computation in the Coq system, Electronic communication of mathematics and the interaction of computer algebra systems and proof assistants, Formal and efficient primality proofs by use of computer algebra oracles, Proof synthesis and reflection for linear arithmetic, Theorem proving modulo, ELAN from a rewriting logic point of view, Dealing with algebraic expressions over a field in Coq using Maple, Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs
Uses Software