Sciweavers

ISMVL
2007
IEEE
119views Hardware» more  ISMVL 2007»
14 years 5 months ago
Automated Reasoning in Some Local Extensions of Ordered Structures
We give a uniform method for automated reasoning in several types of extensions of ordered algebraic structures (definitional extensions, extensions with boundedness axioms or wit...
Viorica Sofronie-Stokkermans, Carsten Ihlemann
TABLEAUX
2009
Springer
14 years 6 months ago
A Novel Architecture for Situation Awareness Systems
Situation Awareness (SA) is the problem of comprehending elements of an environment within a volume of time and space. It is a crucial factor in decision-making in dynamic environm...
Franz Baader, Andreas Bauer 0002, Peter Baumgartne...
CADE
2009
Springer
14 years 6 months ago
A Refined Resolution Calculus for CTL
Lan Zhang, Ullrich Hustadt, Clare Dixon
CADE
2009
Springer
14 years 6 months ago
SPASS Version 3.5
SPASS is an automated theorem prover for full first-order logic with equality and a number of non-classical logics. This system description provides an overview of our recent deve...
Christoph Weidenbach, Dilyana Dimova, Arnaud Fietz...
CADE
2009
Springer
14 years 6 months ago
Interpolant Generation for UTVPI
Abstract. The problem of computing Craig interpolants in SMT has recently received a lot of interest, mainly for its applications in formal verification. Efficient algorithms for ...
Alessandro Cimatti, Alberto Griggio, Roberto Sebas...
CADE
2009
Springer
14 years 6 months ago
Complexity and Algorithms for Monomial and Clausal Predicate Abstraction
predicate abstraction Shuvendu K. Lahiri and Shaz Qadeer Microsoft Research In this paper, we investigate the asymptotic complexity of various predicate abstraction problems relati...
Shuvendu K. Lahiri, Shaz Qadeer
CADE
2001
Springer
14 years 11 months ago
Automated Incremental Termination Proofs for Hierarchically Defined Term Rewriting Systems
We propose the notion of rewriting modules in order to provide a structural and hierarchical approach of TRS. We define then relative dependency pairs built upon these modules whic...
Xavier Urbain
CADE
2001
Springer
14 years 11 months ago
NP-Completeness of Refutability by Literal-Once Resolution
A boolean formula in conjunctive normal form (CNF) F is refuted by literal?once resolution if the empty clause is inferred from F by resolving on each literal of F at most once. Li...
Stefan Szeider
CADE
2001
Springer
14 years 11 months ago
A Top-Down Procedure for Disjunctive Well-Founded Semantics
Abstract. Skepticism is one of the most important semantic intuitions in artificial intelligence. The semantics formalizing skeptical reasoning in (disjunctive) logic programming i...
Kewen Wang
CADE
2001
Springer
14 years 11 months ago
JProver : Integrating Connection-Based Theorem Proving into Interactive Proof Assistants
Abstract. JProver is a first-order intuitionistic theorem prover that creates sequent-style proof objects and can serve as a proof engine in interactive proof assistants with expre...
Stephan Schmitt, Lori Lorigo, Christoph Kreitz, Al...