Author name cluster

Jerzy Marcinkowski

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

9 papers

2 author rows

KR Conference 2025 Conference Paper

About the Multi-Head Linear Restricted Chase Termination

Lukas Gerlach
Lucas Larroque
Jerzy Marcinkowski
Piotr Ostropolski-Nalewaja

The chase is a ubiquitous algorithm in database theory. However, for existential rules (aka tuple-generating dependencies), its termination is not guaranteed, and even undecidable in general. The problem of termination becomes particularly difficult for the restricted (or standard) chase, for which the order of rule application matters. Thus, decidability of restricted chase termination is still open for many well-behaved classes such as linear or guarded multi-headed rules. We make a step forward by showing that all-instances restricted chase termination is decidable in the linear multi-headed case.

PDF Details DOI

KR Conference 2022 Conference Paper

Conservative Extensions for Existential Rules

Jean Christoph Jung
Carsten Lutz
Jerzy Marcinkowski

We study the problem to decide, given sets T1, T2 of tuple-generating dependencies (TGDs), also called existential rules, whether T2 is a conservative extension of T1. We consider two natural notions of conservative extension, one pertaining to answers to conjunctive queries over databases and one to homomorphisms between chased databases. Our main results are that these problems are undecidable for linear TGDs, undecidable for guarded TGDs even when T1 is empty, and decidable for frontier-one TGDs.

PDF Details DOI

CSL Conference 2006 Conference Paper

On the Expressive Power of Graph Logic

Jerzy Marcinkowski

Abstract Graph Logic, a query language being a sublogic of Monadic Second Order Logic is studied in [CGG02]. In the paper [DGG04] the expressiveness power of Graph Logic is examined, and it is shown, for many MSO properties, how to express them in Graph Logic. But despite of the positive examples, it is conjectured there that Graph Logic is strictly less expressive than MSO Logic. Here we give a proof of this conjecture.

Details

LPAR Conference 2004 Conference Paper

On a Semantic Subsumption Test

Jerzy Marcinkowski
Jan Otop
Grzegorz Stelmaszek

Abstract We observe, that subsumption of clauses (in the language of first order logic), so far understood as a syntactic notion, can also be defined by semantical means. Subsumption is NP-complete and testing subsumption takes roughly half of the running time of a typical first order resolution-based theorem prover. We also give some experimental evidence, that replacing syntactic indexing for subsumption by our semantic Monte Carlo technique can, in some situations, significantly decrease the cost of subsumption testing. Finally, we provide some evidence that a similar semantic idea can be probably successfully used for testing for AC matching, which is another NP-complete problem whose millions of instances are being solved by theorem provers.

Details

TCS Journal 2003 Journal Article

Two techniques in the area of the star problem in trace monoids

Daniel Kirsten
Jerzy Marcinkowski

This paper deals with decision problems related to the star problem in trace monoids which means to determine whether the iteration of a recognizable trace language is recognizable. Due to a theorem by Richomme (in: I. Privara et al. (Eds.), MFCS’94 Proc. , Lecture Notes in Computer Science, vol. 841, Springer, Berlin, 1994, pp. 577–586), we know that the star problem is decidable in trace monoids which do not contain a submonoid of the form {a, c}∗×{b, d}∗. [cf. Theory Comput. Systems 34(3) (2001) 193–227]. Here, we consider a more general problem: Is it decidable whether for some recognizable trace language R and some recognizable or finite trace language P the intersection R∩P ∗ is recognizable? If P is recognizable, then we show that this problem is decidable iff the underlying trace monoid does not contain a submonoid of the form {a, c}∗×b∗. In the case of finite languages P, this problem is decidable in {a, c}∗×b∗ but undecidable in {a, c}∗×{b, d}∗.

Details DOI

CSL Conference 2002 Conference Paper

Optimal Complexity Bounds for Positive LTL Games

Jerzy Marcinkowski
Tomasz Truderung

Abstract We prove two tight bounds on complexity of deciding graph games with winning conditions defined by formulas from fragments of LTL. Our first result is that deciding LTL + (◊, ⋀, ∨) games is in PSPACE. This is a tight bound: the problem is known to be PSPACE-hard even for the much weaker logic LTL + (◊, ⋀). We use a method based on a notion of, as we call it, persistent strategy: we prove that in games with positive winning condition the opponent has a winning strategy if and only if he has a persistent winning strategy. The best upper bound one can prove for our problem with the Büchi automata technique, is EXPSPACE. This means that we identify a natural fragment of LTL for which the algorithm resulting from the Büchi automata tool is one exponent worse than optimal. As our second result we show that the problem is EXPSPACE-hard if the winning condition is from the logic LTL + (◊, ○, ⋀, ∨). This solves an open problem from [ AT01 ], where the authors use the Büchi automata technique to show an EXPSPACE algorithm deciding more general LTL (◊, ○, ⋀, ∨) games, but do not prove optimality of this upper bound

Details

CSL Conference 1999 Conference Paper

Directed Reachability: From Ajtai-Fagin to Ehrenfeucht-Fraïssé Games

Jerzy Marcinkowski

Abstract In 1974 Ronald Fagin proved that properties of structures which are in \(\mathcal{N}\mathcal{P}\) are exactly the same as those expressible by existential second order sentences, that is sentences of the form \(\exists \vec P\phi\), where \(\vec P\) is a tuple of relation symbols. and φ is a first order formula. Fagin was also the first to study monadic \(\mathcal{N}\mathcal{P}\): the class of properties expressible by existential second order sentences where all quantified relations are unary. In their very difficult paper [ AF90 ] Ajtai and Fagin show that directed reachability is not in monadic \(\mathcal{N}\mathcal{P}\). In [ AFS97 ] Ajtai, Fagin and Stockmeyer introduce closed monadic \(\mathcal{N}\mathcal{P}\): the class of properties which can be expressed by a kind of monadic second order existential formula, where the second order quantifiers can interleave with first order quantifiers. Among other results they show that directed reachability is expressible by a formula of the form \(x\) φ, where P and P 1 are unary relation symbols and f is first order. They state the question if this property is in the positive first order closure of monadic \(\mathcal{N}\mathcal{P}\), that is if it is expressible by a sentence of the form \(\vec Qx\exists \vec P\phi\), where \(\vec Qx\) is a tuple of first order quantifiers and \(\vec P\) is a tuple of unary relation symbols. In this paper we give a negative solution to the problem.

Details

CSL Conference 1994 Conference Paper

A Horn Clause that Implies and Undecidable Set of Horn Clauses

Jerzy Marcinkowski

Abstract In this paper we prove that there exists a Horn clause H such that the problem: given a Horn clause G. Is G a consequence of H? is not recursive. Equivalently, there exists a one-clause PROLOG program such that there is no PROLOG implementation answering TRUE if the program implies a given goal and FALSE otherwise. We give a short survey of earlier results concerning clause implication and prove a classical Linial-Post theorem as a consequence of one of them.

Details

FOCS Conference 1992 Conference Paper

Undecidability of the Horn-Clause Implication Problem

Jerzy Marcinkowski
Leszek Pacholski

The authors prove that the problem 'given two Horn clauses H/sub 1/=( alpha /sub 1/ V-product alpha /sub 2/ to beta ) and H/sub 2/=( gamma /sub 1/ V-product. .. V-product gamma /sub k/ to delta ), where alpha /sub i/, beta, gamma /sub i/, delta are atomic formulas, decide if H/sub 2/, is a consequence of H/sub 1/' is not recursive. This solves one of the last open decidability problems concerning formulas in pure predicate logic (i. e. without equality symbol). The proof depends on a thorough analysis of derivation trees of one rule of inference with two premisses and one conclusion, and it may have further applications. >

Details