License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.MFCS.2022.30
URN: urn:nbn:de:0030-drops-168285
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/16828/
Go to the corresponding LIPIcs Volume Portal

Chakraborty, Supratik ; Akshay, S.

On Synthesizing Computable Skolem Functions for First Order Logic

pdf-format:
LIPIcs-MFCS-2022-30.pdf (0.8 MB)

Abstract

Skolem functions play a central role in the study of first order logic, both from theoretical and practical perspectives. While every Skolemized formula in first-order logic makes use of Skolem constants and/or functions, not all such Skolem constants and/or functions admit effectively computable interpretations. Indeed, the question of whether there exists an effectively computable interpretation of a Skolem function, and if so, how to automatically synthesize it, is fundamental to their use in several applications, such as planning, strategy synthesis, program synthesis etc.
In this paper, we investigate the computability of Skolem functions and their automated synthesis in the full generality of first order logic. We first show a strong negative result, that even under mild assumptions on the vocabulary, it is impossible to obtain computable interpretations of Skolem functions. We then show a positive result, providing a precise characterization of first-order theories that admit effective interpretations of Skolem functions, and also present algorithms to automatically synthesize such interpretations. We discuss applications of our characterization as well as complexity bounds for Skolem functions (interpreted as Turing machines).

BibTeX - Entry

@InProceedings{chakraborty_et_al:LIPIcs.MFCS.2022.30,
  author =	{Chakraborty, Supratik and Akshay, S.},
  title =	{{On Synthesizing Computable Skolem Functions for First Order Logic}},
  booktitle =	{47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)},
  pages =	{30:1--30:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-256-3},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{241},
  editor =	{Szeider, Stefan and Ganian, Robert and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2022/16828},
  URN =		{urn:nbn:de:0030-drops-168285},
  doi =		{10.4230/LIPIcs.MFCS.2022.30},
  annote =	{Keywords: Skolem functions, Automated, Synthesis, First order logic, Computability}
}

Keywords: Skolem functions, Automated, Synthesis, First order logic, Computability
Collection: 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)
Issue Date: 2022
Date of publication: 22.08.2022

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI