MATH LP (LIT Project)

Project Lead

Project Duration

01/08/2020 - 28/02/2023

Partners

Publications

2021

[Cerna]

A Special Case of Schematic Syntactic Unification

David M. Cerna

CAS ICS / RISC. Technical report, 2021. [pdf]
[bib]
@techreport{RISC6349,
author = {David M. Cerna},
title = {{A Special Case of Schematic Syntactic Unification}},
language = {english},
abstract = {We present a unification problem based on first-order syntactic unification which ask whether every problemin a schematically-defined sequence of unification problems isunifiable, so called loop unification. Alternatively, our problemmay be formulated as a recursive procedure calling first-ordersyntactic unification on certain bindings occurring in the solvedform resulting from unification. Loop unification is closely relatedto Narrowing as the schematic constructions can be seen as arewrite rule applied during unification, and primal grammars, aswe deal with recursive term constructions. However, loop unifi-cation relaxes the restrictions put on variables as fresh as wellas used extra variables may be introduced by rewriting. In thiswork we consider an important special case, so called semiloopunification. We provide a sufficient condition for unifiability of theentire sequence based on the structure of a sufficiently long initialsegment. It remains an open question whether this conditionis also necessary for semiloop unification and how it may beextended to loop unification.},
year = {2021},
institution = {CAS ICS / RISC},
length = {8}
}
[Cerna]

Learning Higher-Order Programs without Meta-Interpretive Learning

Stanislav Purgal and David Cerna and Cezary Kalisyk

Technical report no. 21-22 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). December 2021. Licensed under CC BY 4.0 International. [doi] [pdf]
[bib]
@techreport{RISC6393,
author = {Stanislav Purgal and David Cerna and Cezary Kalisyk},
title = {{Learning Higher-Order Programs without Meta-Interpretive Learning}},
language = {english},
abstract = {Learning complex programs through textit{inductive logic programming} (ILP) remains a formidable challenge. Existing higher-order enabled ILP systems show improved accuracy and learning performance, though remain hampered by the limitations of the underlying learning mechanism. Experimental results show that our extension of the versatile textit{Learning From Failures} paradigm by higher-order definitions significantly improves learning performance without the burdensome human guidance required by existing systems. Furthermore, we provide a theoretical framework capturing the class of higher-order definitions handled by our extension.},
number = {21-22},
year = {2021},
month = {December},
keywords = {Inductive Logic Programming, Higher order definitions},
length = {8},
license = {CC BY 4.0 International},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}

2020

[Cerna]

Anti-unification and the Theory of Semirings

David M. Cerna

Theor. Comput. Sci. 848, pp. 133-139. 2020. RISC / CAS ICS, 0304-3975. [doi]
[bib]
@article{RISC6234,
author = {David M. Cerna},
title = {{Anti-unification and the Theory of Semirings}},
language = {english},
abstract = {It was recently shown that anti-unification over an equational theory consisting of only unitequations (more than one) is nullary. Such pure theories are artificial and are of little effect onpractical aspects of anti-unification. In this work, we extend these nullarity results to the theory ofsemirings, a heavily studied theory with many practical applications. Furthermore, our argumentholds over semirings with commutative multiplication and/or idempotent addition. We also cover afew open questions discussed in previous work.},
journal = {Theor. Comput. Sci.},
volume = {848},
pages = {133--139},
isbn_issn = {0304-3975},
year = {2020},
refereed = {yes},
institution = {RISC / CAS ICS},
length = {7},
url = {https://doi.org/10.1016/j.tcs.2020.10.020}
}
[Cerna]

Schematic Refutations of Formula Schemata

David Cerna and Alexander Leitsch and Anela Lolic

Journal of Automated Reasoning, pp. -. 2020. 1573-0670. [doi]
[bib]
@article{RISC6235,
author = {David Cerna and Alexander Leitsch and Anela Lolic},
title = {{Schematic Refutations of Formula Schemata}},
language = {english},
abstract = {Proof schemata are infinite sequences of proofs which are defined inductively. In this paper we present a general framework for schemata of terms, formulas and unifiers and define a resolution calculus for schemata of quantifier-free formulas. The new calculus generalizes and improves former approaches to schematic deduction. As an application of the method we present a schematic refutation formalizing a proof of a weak form of the pigeon hole principle.},
journal = {Journal of Automated Reasoning},
pages = {--},
isbn_issn = {1573-0670},
year = {2020},
refereed = {yes},
length = {47},
url = {https://doi.org/10.1007/s10817-020-09583-8}
}

Loading…