Logic Program Termination Analysis Using Atom Sizes

Authors: Marco Calautti, Sergio Greco, Cristian Molinaro, Irina Trubitsyna

IJCAI 2015 | Conference PDF | Archive PDF | Plain Text | LLM Run Details

Reproducibility Variable Result LLM Response
Research Type Theoretical In this paper, we propose a novel class of logic programs whose evaluation always terminates. The proposed technique identifies terminating programs that are not captured by any of the current approaches. Our technique is based on the idea of measuring the size of terms and atoms to check whether the rule head size is bounded by the body, and performs a more fine-grained analysis than previous work. Rather than adopting an all-or-nothing approach (either we can say that the program is terminating or we cannot say anything), our technique can identify arguments that are limited (i.e., where there is no infinite propagation of terms) even when the program is not entirely recognized as terminating. Identifying arguments that are limited can support the user in the problem formulation and help other techniques that use limited arguments as a starting point. Another useful feature of our approach is that it is able to leverage external information about limited arguments. We also provide results on the correctness, the complexity, and the expressivity of our technique.
Researcher Affiliation Academia Marco Calautti, Sergio Greco, Cristian Molinaro, Irina Trubitsyna DIMES, Universit a della Calabria 87036 Rende (CS), Italy {calautti,greco,molinaro,trubitsyna}@dimes.unical.it
Pseudocode No The paper includes definitions and examples of logic programs, but does not present any structured pseudocode or algorithm blocks.
Open Source Code No The paper does not provide any concrete access to source code for the methodology described, nor does it explicitly state that code is released or available.
Open Datasets No The paper is theoretical and does not involve empirical studies with datasets; therefore, there is no information about training data availability.
Dataset Splits No The paper is theoretical and does not involve empirical studies with datasets; therefore, no dataset split information for training, validation, or testing is provided.
Hardware Specification No The paper does not provide any specific hardware details used for running experiments.
Software Dependencies No The paper does not specify any software dependencies with version numbers needed to replicate the work.
Experiment Setup No The paper is theoretical and does not describe empirical experiments, therefore no experimental setup details like hyperparameters or system-level training settings are provided.