197
click to vote
CADE
2015
Springer
9 years 11 months ago
2015
Springer
Abstract. Hereditarily finite (HF) set theory provides a standard universe of sets, but with no infinite sets. Its utility is demonstrated through a formalisation of the theory o...
114
click to vote
CADE
2015
Springer
9 years 11 months ago
2015
Springer
KeYmaera X is a theorem prover for differential dynamic logic (dL), a logic for specifying and verifying properties of hybrid systems. Reasoning about complicated hybrid systems mo...
139
click to vote
CADE
2015
Springer
9 years 11 months ago
2015
Springer
Abstract. We describe an executable specification and a total correctness proof of a King and Rook vs King (KRK) chess endgame strategy within the proof assistant Isabelle/HOL. Th...
109
click to vote
CADE
2015
Springer
9 years 11 months ago
2015
Springer
Lean is a new open source theorem prover being developed at Microsoft Research and Carnegie Mellon University, with a small trusted kernel based on dependent type theory. It aims t...
124
click to vote
CADE
2015
Springer
9 years 11 months ago
2015
Springer
Our computational metaphysics group describes its use of automated reasoning tools to study Leibniz’s theory of concepts. We start with a reconstruction of Leibniz’s theory wi...