Sciweavers

Share
warning: Creating default object from empty value in /var/www/modules/taxonomy/taxonomy.module on line 1416.
FROCOS
2009
Springer
11 years 9 months ago
Efficient Combination of Decision Procedures for MUS Computation
In recent years, the problem of extracting a MUS (Minimal Unsatisfiable Subformula) from an unsatisfiable CNF has received much attention. Indeed, when a Boolean formula is proved ...
Cédric Piette, Youssef Hamadi, Lakhdar Sais
FROCOS
2009
Springer
11 years 9 months ago
Unification Modulo Homomorphic Encryption
Siva Anantharaman, Hai Lin, Christopher Lynch, Pal...
FROCOS
2009
Springer
11 years 9 months ago
A Declarative Agent Programming Language Based on Action Theories
We discuss a new concept of agent programs that combines logic programming with reasoning about actions. These agent logic programs are characterized by a clear separation between ...
Conrad Drescher, Stephan Schiffel, Michael Thielsc...
FROCOS
2009
Springer
11 years 11 months ago
Runtime Verification Using a Temporal Description Logic
Franz Baader, Andreas Bauer 0002, Marcel Lippmann
FROCOS
2009
Springer
11 years 11 months ago
Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme
In an attempt to improve automation capabilities in the Coq proof assistant, we develop a tactic for the propositional fragment based on the DPLL procedure. Although formulas natur...
Stéphane Lescuyer, Sylvain Conchon
FROCOS
2009
Springer
11 years 11 months ago
Automating Theories in Intuitionistic Logic
Deduction modulo consists in applying the inference rules of a deductive system modulo a rewrite system over terms and formulæ. This is equivalent to proving within a so-called co...
Guillaume Burel
FROCOS
2009
Springer
11 years 11 months ago
Combining Instance Generation and Resolution
Christopher Lynch, Ralph Eric McGregor
FROCOS
2009
Springer
11 years 11 months ago
Argument Filterings and Usable Rules for Simply Typed Dependency Pairs
d abstract) Takahito Aoto† Toshiyuki Yamada‡
Takahito Aoto, Toshiyuki Yamada
books