SNARK

• First-order theorem prover

• Agenda-based with set of support and ordering restriction

• Equality reasoning

• Developed at SRI by Mark Stickel for 15-20 years

• Solid and stable inference engine

Previous slide

Next slide

Back to first slide

View graphic version