6 citations · 6 across the 1 of their papers we have counts for
3 papers
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…
Language and Proofs for Higher-Order SMT (Work in Progress)
Haniel Barbosa, Jasmin Christian Blanchette, Simon Cruanes +2
Satisfiability modulo theories (SMT) solvers have throughout the years been able to cope with increasingly expressive formulas, from ground logics to full first-order logic modulo…
Extending Nunchaku to Dependent Type Theory
Simon Cruanes, Jasmin Christian Blanchette
Nunchaku is a new higher-order counterexample generator based on a sequence of transformations from polymorphic higher-order logic to first-order logic. Unlike its predecessor Nitp…