Autumn School

12 - 13 September 2025

Students and researchers interested in topics in logic programming are invited to attend the 2025 School on Logic Programming. It will take place on September 12 and 13, 2025, during the 41st International Conference on Logic Programming (September 12--19, 2025, University of Calabria, Italy).

The 2-day school is suited for those who wish to learn advanced topics in logic programming and constraint programming.

Format

The school will consist of four tutorials, of one hour each, two on Friday, September 12, and two on Saturday, September 13.

The schedule is part of the DC program and will not overlap with the workshops on those days so that ICLP attendees participating in the workshop can also attend the School talks.

Schedule

Room: DEMACS, Cubo 30B, Room MT10

Fri 12/09/2025

12:00-13:00 Mario Alviano (University of Calabria, Italy)

Programming with Templates and LLMs: The ASP Chef Approach

Answer Set Programming (ASP) can be greatly enhanced by integrating it with Large Language Models (LLMs), especially when answer sets are transformed into structured prompts and outputs. In this talk, I present how ASP Chef uses Mustache templates to generate prompts, configuration files, tables, forms, and graphs directly from ASP results. These templates extract data via ASP queries and produce inputs suitable for LLMs. For example, we can generate a prompt asking the LLM to answer in CSV format, and then manipulate the resulting CSV using ASP Chef ingredients. This approach enables smooth interaction with external systems and allows declarative post-processing of LLM outputs, bridging symbolic reasoning with modern AI workflows.

14:00-15:00 Pedro Cabalar (Universidade da Coruña, Spain)

A tour around Here and There

When compared to other approaches in AI, correctness still stands as the main strength of logic-based knowledge representation and reasoning. A logical characterization of a formal language provides a mathematical tool that can help us to justify or explain a given result, to prove correctness of a given implementation or to perform formal analyses such as equivalence among difference representations. But sometimes, in practice, a more significant advantage of a logical characterization is its invaluable role as a guide for the semantics of new language extensions. In this tutorial, we will focus on the logical characterization of Answer Set Programming (ASP) based on Equilibrium Logic and its monotonic basis, the intermediate logic of Here-and-There (HT). We will explain the basic definitions, both for propositional and first-order HT, and explore some of the most interesting results related to ASP, such as the application to strong equivalence or the formalization of aggregates. We will also quickly overview some of the main ASP extensions based on HT such as temporal ASP, epistemic ASP, or the use of evaluable functions and numerical constraints.

Sat 13/09/2025

12:00-13:00 Fred Mesnard (Universite de la Réunion, France)

Interactive proofs for logic programs

In this tutorial, we present LPTP, a Logic Programming Theorem Prover designed and written by Robert Staerk in the late 1990’s. LPTP is an interactive environment which allows to build and check proofs of properties of logic programs, including types, groundness, invariants, universal left termination, and equivalence of predicates. We also summarize our recent works blending LPTP with automated theorem proving and abstract interpretation.

14:00-15:00 Włodek Drabent (Polish Academy of Sciences, Poland)

It is declarative

On reasoning about logic programs and constructing them

Logic programming was invented as a declarative programming paradigm. However Prolog programmers often neglect the logic, and use Prolog as an imperative language with unconventional control and other unusual features. We show how to reason about logic programs declaratively, i.e. in terms of their logical semantics, hence abstracting from the control. We present proof methods for program correctness and completeness. (Correctness means that the answers produced by the program are compatible with the specification, completeness - that whatever the specification requires is an answer of a program.) In this lecture we deal with programs without negation.

Out of these proof methods one can derive methods of declarative diagnosis of programs (algorithmic debugging), and an approach of systematic construction of programs. We argue that the discussed methods are applicable, possibly at informal level, in practical every-day programming.