{'fraction_non_alphanumeric': 0.02525523911875336, 'fraction_numerical': 0.0, 'mean_word_length': 5.442906574394463, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Characterising Relativised Strong Equivalence with Projection for Non-Ground Logic Programs

This thesis deals with advanced notions of equivalence between logic programs under answer-set semantics. Particularly, we generalise the concepts of relativised strong equivalence and relativised strong equivalence with projection to the non-ground case, i.e., to programs with variables. In recent work, a framework for expressing equivalences between answer-set programs was introduced and later generalised for non-ground programs. These works use said framework to characterise a fine-grained version of strong equivalence. For two programs to be (ordinarly) equivalent, they just have to have the same answer sets. In contrast, two programs are strongly equivalent if it is possible to add the same arbitray rules to both of them and their answer sets still match. In other words, if the (sub)programs P and Q are strongly equivalent, then P can be replaced with Q in any context program. The equivalence notion we are concerned with extends strong equivalence by enabling the restriction of the predicates of the context programs and the filtering of auxiliary predicates. Like already mentioned, this version of equivalence is called relativised strong equivalence with projection and was so far only studied for propositional (or ground) programs. Aside from characterising relativised strong equivalence (with projection) for the non-ground case in the mentioned framework, we also provide model-theoretic characterisations for the non-ground setting. In particular, we introduce the generalization of a structure which captures relativised strong equivalence, namely the so-called RSE-model. Furthermore, we provide liftings of a spoiler and a counterexample, two structures used for checking relativised strong equivalence with projection between programs.