enter search term and/or author name
Infons are statements viewed as containers of information (rather then representations of truth values). The logic of infons turns out to be a conservative extension of logic known as constructive or intuitionistic. Distributed Knowledge...
A data word is a sequence of pairs of a letter from a finite alphabet and an element from an infinite set, where the latter can only be compared for equality. Safety one-way alternating automata with one register on infinite data words are...
Well-founded semantics for description logic programs in the semantic web
Thomas Eiter, Giovambattista Ianni, Thomas Lukasiewicz, Roman Schindlauer
Article No.: 11
The realization of the Semantic Web vision, in which computational logic has a prominent role, has stimulated a lot of research on combining rules and ontologies, which are formulated in different formalisms. In particular, combining logic...
Monadic second order logic on graphs with local cardinality constraints
Article No.: 12
We introduce the class of MSO-LCC problems, which are problems of the following form. Given a graph G and for each vertex v of G a set α(v) of non-negative integers. Is there a set S of vertices or edges of...
The tractability of model checking for LTL: The good, the bad, and the ugly fragments
Michael Bauland, Martin Mundhenk, Thomas Schneider, Henning Schnoor, Ilka Schnoor, Heribert Vollmer
Article No.: 13
In a seminal paper from 1985, Sistla and Clarke showed that the model-checking problem for Linear Temporal Logic (LTL) is either NP-complete or PSPACE-complete, depending on the set of temporal operators used. If in contrast, the set of...
The semantics of most logics of time and probability is given via a probability distribution over threads, where a thread is a structure specifying what will be true at different points in time (in the future). When assessing the...
LF is a dependent type theory in which many other formal systems can be conveniently embedded. However, correct use of LF relies on nontrivial metatheoretic developments such as proofs of correctness of decision procedures for LF's judgments....
Persistent queries in the behavioral theory of algorithms
Andreas Blass, Yuri Gurevich
Article No.: 16
We propose an extension of the behavioral theory of interactive sequential algorithms to deal with the following situation. A query is issued during a certain step, but the step ends before any reply is received. Later, a reply arrives, and later...
MWeb: A principled framework for modular web rule bases and its semantics
Anastasia Analyti, Grigoris Antoniou, Carlos Viegas Damasio
Article No.: 17
We present a principled framework for modular Web rule bases, called MWeb. According to this framework, each predicate defined in a rule base is characterized by its defining reasoning mode, scope, and exporting rule base list. Each predicate used...