CADE
2010
Springer
14 years 29 days ago
2010
Springer
iProver-Eq is an implementation of an instantiation-based calculus Inst-Gen-Eq which is complete for first-order logic with equality. iProver-Eq extends the iProver system with sup...
CADE
2010
Springer
14 years 29 days ago
2010
Springer
Abstract. Symbolic reasoning is in the core of many software development tools such as: bug-finders, test-case generators, and verifiers. Of renewed interest is the use of symbolic...
CADE
2010
Springer
14 years 29 days ago
2010
Springer
Abstract. We describe mcmt, a fully declarative and deductive symbolic model checker for safety properties of infinite state systems whose state variables are arrays. Theories spec...
CADE
2010
Springer
14 years 29 days ago
2010
Springer
Coalgebraic description logics offer a common semantic umbrella for extensions of description logics with reasoning principles outside relational semantics, e.g. quantitative uncer...
CADE
2010
Springer
14 years 29 days ago
2010
Springer
Automated software verification and path-sensitive program analysis require the ability to distinguish executable program paths from those that are infeasible. To achieve this, pro...
CADE
2010
Springer
14 years 29 days ago
2010
Springer
Abstract. Sledgehammer, a component of the interactive theorem prover Isabelle, finds proofs in higher-order logic by calling the automated provers for first-order logic E, SPASS a...
CADE
2010
Springer
14 years 29 days ago
2010
Springer
We consider security properties of cryptographic protocols, that are either trace properties (such as confidentiality or authenticity) or equivalence properties (such as anonymity ...
CADE
2010
Springer
14 years 29 days ago
2010
Springer
We propose an extension of the syntactic restriction for complex role inclusion axioms in the description logic SROIQ. Like the original restriction in SROIQ, our restrictions can ...
CADE
2010
Springer
14 years 29 days ago
2010
Springer
This system description provides an overview of the MUNCH reasoner for sets and multisets. MUNCH takes as the input a formula in a logic that supports expressions about sets, multi...
CADE
2010
Springer
14 years 29 days ago
2010
Springer
Abstract. Automated theorem provers (ATPs) struggle to solve problems with large sets of possibly superfluous axiom. Several algorithms have been developed to reduce the number of ...