211
click to vote
CADE
2015
Springer
9 years 11 months ago
2015
Springer
Beagle is an automated theorem prover for first-order logic modulo built-in theories. It implements a refined version of the hierarchic superposition calculus. This system descri...
191
Voted
CADE
2015
Springer
9 years 11 months ago
2015
Springer
Abstract. We present a decision procedure that combines reasoning about datatypes and codatatypes. The dual of the acyclicity rule for datatypes is a uniqueness rule that identifi...
182
click to vote
CADE
2015
Springer
9 years 11 months ago
2015
Springer
Abstract. The termination competition focuses on automated termination analysis for all kinds of programming paradigms, including categories for term rewriting, imperative programm...
177
click to vote
CADE
2015
Springer
9 years 11 months ago
2015
Springer
Abstract. We present a method and an associated system, called MathCheck, that embeds the functionality of a computer algebra system (CAS) within the inner loop of a conflict-driv...