Sciweavers

JANCL
2006
74views more  JANCL 2006»
13 years 11 months ago
Linear-time temporal logics with Presburger constraints: an overview
We present an overview of linear-time temporal logics with Presburger constraints whose models are sequences of tuples of integers. Such formal specification languages are welldesi...
Stéphane Demri
JANCL
2006
100views more  JANCL 2006»
13 years 11 months ago
An efficient relational deductive system for propositional non-classical logics
We describe a relational framework that uniformly supports formalization and automated reasoning in various propositional modal logics. The proof system we propose is a relational ...
Andrea Formisano, Marianna Nicolosi Asmundo
JANCL
2006
105views more  JANCL 2006»
13 years 11 months ago
BDD-based decision procedures for the modal logic K
We describe BDD-based decision procedures for the modal logic K. Our approach is inspired by the automata-theoretic approach, but we avoid explicit automata construction. Instead, ...
Guoqiang Pan, Ulrike Sattler, Moshe Y. Vardi
JANCL
2006
65views more  JANCL 2006»
13 years 11 months ago
SUBSEXPL: a tool for simulating and comparing explicit substitutions calculi
Flávio L. C. de Moura, Mauricio Ayala-Rinc&...
JANCL
2006
123views more  JANCL 2006»
13 years 11 months ago
Approximate databases: a support tool for approximate reasoning
This paper describes an experimental platform for approximate knowledge databases called the Approximate Knowledge Database (AKDB), based on a semantics inspired by rough sets. The...
Patrick Doherty, Martin Magnusson, Andrzej Szalas
JANCL
2006
112views more  JANCL 2006»
13 years 11 months ago
KAT-ML: an interactive theorem prover for Kleene algebra with tests
We describe KAT-ML, an implementation of an interactive theorem prover for Kleene algebra with tests (KAT). The system is designed to reflect the natural style of reasoning with K...
Kamal Aboul-Hosn, Dexter Kozen