CADE
2008
Springer
14 years 11 months ago
2008
Springer
We describe a framework with which first order theorem provers can be used for checking formal proofs. The main aim of the framework is to take as much advantage as possible from t...
CADE
2008
Springer
14 years 11 months ago
2008
Springer
Abstract. This paper describes the translation of proofs in the Thousands of Solutions from Theorem Provers (TSTP) solution library to the Proof Markup Language (PML), and the subs...
CADE
2008
Springer
14 years 11 months ago
2008
Springer
This paper describes the integration of the ATP support of the TPTPWorld into the Sigma Knowledge Engineering Environment. The result is an interactive knowledge based reasoning en...
CADE
2008
Springer
14 years 11 months ago
2008
Springer
Abstract. We implement an algorithm for extracting appropriate collections of classic-like sound and complete tableaux rules for a large class of finite-valued logics. Its output c...
CADE
2008
Springer
14 years 11 months ago
2008
Springer
Previous CASC competitions have focused on proving difficult problems on small numbers of axioms. However, typical reasoning applications for expert systems rely on knowledge base...
CADE
2008
Springer
14 years 11 months ago
2008
Springer
Abstract. We present randoCoP, a theorem prover for classical firstorder logic, which integrates randomized search techniques into the connection prover leanCoP 2.0. By randomly re...
CADE
2008
Springer
14 years 11 months ago
2008
Springer
We present a novel proof of Toyama's famous modularity of confluence result for term rewriting systems. Apart from being short and intuitive, the proof is modular itself in th...
CADE
2008
Springer
14 years 11 months ago
2008
Springer
Abstract. In this paper we describe a new tool for performing KnuthBendix completion with automatic termination tools. It is based on two ingredients: (1) the inference system for ...
CADE
2008
Springer
14 years 11 months ago
2008
Springer
We propose a procedure for automated implicit inductive theorem proving for equational specifications made of rewrite rules with conditions and constraints. The constraints are int...
CADE
2008
Springer
14 years 11 months ago
2008
Springer
This paper describes a system combining model-based and learning-based methods for automated reasoning in large theories, i.e. on a large number of problems that use many axioms, l...