Sciweavers

Share
warning: Creating default object from empty value in /var/www/modules/taxonomy/taxonomy.module on line 1416.
CADE
2010
Springer
10 years 10 months ago
Terminating Tableaux for Hybrid Logic with Eventualities
x-free and employs a novel clausal form that abstracts away from propositional reasoning. It comes with an elegant correctness proof. We discuss some optimizations for decision pro...
Mark Kaminski, Gert Smolka
CADE
2010
Springer
10 years 10 months ago
On Hierarchical Reasoning in Combinations of Theories
Carsten Ihlemann, Viorica Sofronie-Stokkermans
CADE
2010
Springer
10 years 11 months ago
Verifying Safety Properties with the TLA+ Proof System
Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport,...
CADE
2010
Springer
10 years 11 months ago
Monotonicity Criteria for Polynomial Interpretations over the Naturals
Polynomial interpretations are a useful technique for proving termination of term rewrite systems. In an automated setting, termination tools are concerned with parametric polynomi...
Friedrich Neurauter, Aart Middeldorp, Harald Zankl
CADE
2010
Springer
11 years 1 months ago
Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)
Beluga is an environment for programming and reasoning about formal systems given by axioms and inference rules. It implements the logical framework LF for specifying and prototypi...
Brigitte Pientka, Joshua Dunfield
CADE
2010
Springer
11 years 1 months ago
Optimized Description Logic Reasoning via Core Blocking
State of the art reasoners for expressive description logics, such as those that underpin the OWL ontology language, are typically based on highly optimized implementations of (hyp...
Birte Glimm, Ian Horrocks, Boris Motik
CADE
2010
Springer
11 years 1 months ago
Tractable Extensions of the Description Logic EL with Numerical Datatypes
Despoina Magka, Yevgeny Kazakov, Ian Horrocks
CADE
2010
Springer
11 years 1 months ago
A Decision Procedure for CTL* Based on Tableaux and Automata
Oliver Friedmann, Markus Latte, Martin Lange
CADE
2010
Springer
11 years 1 months ago
An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic
Craig interpolation has become a versatile tool in formal verification, for instance to generate intermediate assertions for safety analysis of programs. Interpolants are typically...
Angelo Brillout, Daniel Kroening, Philipp Rüm...
CADE
2010
Springer
11 years 1 months ago
Analytic Tableaux for Higher-Order Logic with Choice
Abstract. While many higher-order interactive theorem provers include a choice operator, higher-order automated theorem provers currently do not. As a step towards supporting autom...
Julian Backes, Chad E. Brown
books