MATH LP (LIT Project)
Project Lead
Project Duration
01/08/2020 - 28/02/2023
Partners
JKU
Publications
2022
[Cerna]
Learning Higher-Order Programs without Meta-Interpretive Learning
Stanislav Purgal and David Cerna and Cezary Kalisyk
In: Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence, IJCAI-22, Lud De Raedt (ed.), Proceedings of International Joint Conference on Artificial Intelligence, Main Track , pp. 2726-2733. july 2022. International Joint Conferences on Artificial Intelligence Organization, 10.24963/ijcai.2022/378. [doi]@inproceedings{RISC6646,
author = {Stanislav Purgal and David Cerna and Cezary Kalisyk},
title = {{Learning Higher-Order Programs without Meta-Interpretive Learning}},
booktitle = {{Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence, IJCAI-22}},
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.},
series = {Main Track},
pages = {2726--2733},
publisher = {International Joint Conferences on Artificial Intelligence Organization},
isbn_issn = {10.24963/ijcai.2022/378},
year = {2022},
month = {july},
editor = {Lud De Raedt},
refereed = {yes},
keywords = {Inductive Logic Programming, Higher order definitions},
length = {8},
conferencename = {International Joint Conference on Artificial Intelligence},
url = {https://doi.org/10.35011/risc.21-22}
}
author = {Stanislav Purgal and David Cerna and Cezary Kalisyk},
title = {{Learning Higher-Order Programs without Meta-Interpretive Learning}},
booktitle = {{Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence, IJCAI-22}},
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.},
series = {Main Track},
pages = {2726--2733},
publisher = {International Joint Conferences on Artificial Intelligence Organization},
isbn_issn = {10.24963/ijcai.2022/378},
year = {2022},
month = {july},
editor = {Lud De Raedt},
refereed = {yes},
keywords = {Inductive Logic Programming, Higher order definitions},
length = {8},
conferencename = {International Joint Conference on Artificial Intelligence},
url = {https://doi.org/10.35011/risc.21-22}
}
2021
[Cerna]
A Special Case of Schematic Syntactic Unification
David M. Cerna
CAS ICS / RISC. Technical report, 2021. [pdf]@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}
}
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}
}
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]@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}
}
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]@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}
}
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}
}
