CADE
2005
Springer
14 years 11 months ago
2005
Springer
Proof planning is an automated reasoning technique which improves proof search by raising it to a meta-level. In this paper we apply proof planning to First-Order Linear Temporal L...
CADE
2005
Springer
14 years 11 months ago
2005
Springer
Abstract. We describe methods for automated theorem proving in extensional type theory with primitive equality. We discuss a complete, cut-free sequent calculus as well as a compac...
CADE
2005
Springer
14 years 11 months ago
2005
Springer
Our general goal is to provide better automation in interactive proof assistants such as Coq. We present an interpreter of proof traces in first-order multi-sorted logic with equal...
CADE
2005
Springer
14 years 11 months ago
2005
Springer
CADE
2005
Springer
14 years 11 months ago
2005
Springer
Abstract. Basically, the connection of two many-sorted theories is obtained by taking their disjoint union, and then connecting the two parts through connection functions that must...
CADE
2005
Springer
14 years 11 months ago
2005
Springer
We present sKizzo, a system designed to evaluate and certify Quantified Boolean Formulas (QBFs) by means of propositional skolemization and symbolic reasoning.
CADE
2005
Springer
14 years 11 months ago
2005
Springer
Abstract. We describe the instance store, a system for reasoning about individuals (i.e., instances of classes) in OWL ontologies. By using a hybrid reasoner/database architecture,...
CADE
2005
Springer
14 years 11 months ago
2005
Springer
In many theorem proving applications, a proper treatment of equational theories or equality is mandatory. In this paper we show how to integrate a modern treatment of equality in ...