Sciweavers

Share
CADE
2015
Springer
4 years 2 months ago
KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems
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...
Nathan Fulton, Stefan Mitsch, Jan-David Quesel, Ma...
CADE
2015
Springer
4 years 2 months ago
Proving Correctness of a KRK Chess Endgame Strategy by Using Isabelle/HOL and Z3
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...
Filip Maric, Predrag Janicic, Marko Malikovic
CADE
2015
Springer
4 years 2 months ago
The Lean Theorem Prover (System Description)
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...
Leonardo Mendonça de Moura, Soonho Kong, Je...
CADE
2015
Springer
4 years 2 months ago
Automating Leibniz's Theory of Concepts
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...
Jesse Alama, Paul E. Oppenheimer, Edward N. Zalta
CADE
2015
Springer
4 years 2 months ago
Interactive Theorem Proving - Modelling the User in the Proof Process
Proving complex problems requires user interaction during proof construction. A major prerequisite for user interaction is that the user is able to understand the proof state in or...
Bernhard Beckert, Sarah Grebing
CADE
2015
Springer
4 years 2 months ago
Expressing Symmetry Breaking in DRAT Proofs
An effective SAT preprocessing technique is the addition of symmetry-breaking predicates: auxiliary clauses that guide a SAT solver away from needless exploration of isomorphic su...
Marijn Heule, Warren A. Hunt Jr., Nathan Wetzler
CADE
2015
Springer
4 years 2 months ago
SMTtoTPTP - A Converter for Theorem Proving Formats
SMTtoTPTP is a converter from proof problems written in the SMT-LIB format into the TPTP TFF format. The SMT-LIB format supports polymorphic sorts and frequently used theories like...
Peter Baumgartner
CADE
2015
Springer
4 years 2 months ago
Program Synthesis Using Dual Interpretation
Abstract. We present an approach to component-based program synthesis that uses two distinct interpretations for the symbols in the program. The first interpretation defines the ...
Ashish Tiwari, Adria Gascón, Bruno Dutertre
CADE
2015
Springer
4 years 2 months ago
Decidability of Univariate Real Algebra with Predicates for Rational and Integer Powers
We prove decidability of univariate real algebra extended with predicates for rational and integer powers, i.e., “xn ∈ Q” and “xn ∈ Z.” Our decision procedure combines ...
Grant Olney Passmore
CADE
2013
Springer
6 years 2 months ago
One Logic to Use Them All
Deductive program verication is making fast progress these days. One of the reasons is a tremendous improvement of theorem provers in the last two decades. This includes various k...
Jean-Christophe Filliâtre
books