3 papers
cs.LO2020
Proceedings of the Sixteenth International Workshop on the ACL2 Theorem Prover and its Applications
Grant Passmore, Ruben Gamboa
This volume contains a selection of papers presented at the 16th International Workshop on the ACL2 Theorem Prover and its Applications (ACL2-2020). The workshops are the premier t…
cs.LO2020
The Imandra Automated Reasoning System (system description)
Grant Olney Passmore, Simon Cruanes, Denis Ignatovich +6
We describe Imandra, a modern computational logic theorem prover designed to bridge the gap between decision procedures such as SMT, semi-automatic inductive provers of the Boyer-M…
math.LO2015
Decidability of Univariate Real Algebra with Predicates for Rational and Integer Powers
Grant Olney Passmore
We prove decidability of univariate real algebra extended with predicates for rational and integer powers, i.e., and . Our decision pro…