8 citations · 15 across the 3 of their papers we have counts for
4 papers
Superposition for Lambda-Free Higher-Order Logic
Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes +1
We introduce refutationally complete superposition calculi for intentional and extensional clausal -free higher-order logic, two formalisms that allow partial application and ap…
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…