enter search term and/or author name
Logical queries over views: Decidability and expressiveness
James Bailey, Guozhu Dong, Anthony WIDJAJA To
Article No.: 8
We study the problem of deciding the satisfiability of first-order logic queries over views, with our aim to delimit the boundary between the decidable and the undecidable fragments of this language. Views currently occupy a central place in...
Deciding security properties for cryptographic protocols. application to key cycles
Hubert Comon-Lundh, Véronique Cortier, Eugen Zălinescu
Article No.: 9
There is a large amount of work dedicated to the formal verification of security protocols. In this article, we revisit and extend the NP-complete decision procedure for a bounded number of sessions. We use a, now standard, deducibility constraint...
Real-world use of RDF requires the ability to transparently represent and explain metadata associated with RDF triples. For example, when RDF triples are extracted automatically by information extraction programs, there is a need to represent...
Weyl's predicative classical mathematics as a logic-enriched type theory
Robin Adams, Zhaohui Luo
Article No.: 11
We construct a logic-enriched type theory LTTW that corresponds closely to the predicative system of foundations presented by Hermann Weyl in Das Kontinuum. We formalize many results from that book in LTTW, including...
Undecidability and intractability results concerning datalog programs and their persistency numbers
Stavros Cosmadakis, Eugenie Foustoucos, Anastasios Sidiropoulos
Article No.: 12
The relation between Datalog programs and homomorphism problems, and, between Datalog programs and bounded treewidth structures has been recognized for some time and given much attention recently. Additionally, the essential role of persistent...
Proof search specifications of bisimulation and modal logics for the π-calculus
Alwen Tiu, Dale Miller
Article No.: 13
We specify the operational semantics and bisimulation relations for the finite π-calculus within a logic that contains the ∇ quantifier for encoding generic judgments and definitions for encoding fixed points. Since we restrict to...
FDNC: Decidable nonmonotonic disjunctive logic programs with function symbols
Thomas Eiter, Mantas Šimkus
Article No.: 14
We present the class FDNC of logic programs that allows for function symbols (F), disjunction (D), nonmonotonic negation under the answer set semantics (N), and constraints (C), while still retaining the decidability of the standard reasoning...