Related papers: An Encoding for CLP Problems in SMT-LIB
Logic programming with tabling and constraints (TCLP, tabled constraint logic programming) has been shown to be more expressive and in some cases more efficient than LP, CLP or LP + tabling. Previous designs of TCLP systems did not fully…
ECLiPSe is a Prolog-based programming system, aimed at the development and deployment of constraint programming applications. It is also used for teaching most aspects of combinatorial problem solving, e.g. problem modelling, constraint…
{log} (read 'setlog') was born as a Constraint Logic Programming (CLP) language where sets and binary relations are first-class citizens, thus fostering set programming. Internally, {log} is a constraint satisfiability solver implementing…
Concolic testing mixes symbolic and concrete execution to generate test cases covering paths effectively. Its benefits have been demonstrated for more than 15 years to test imperative programs. Other programming paradigms, like logic…
Formal reasoning about finite sets and cardinality is an important tool for many applications, including software verification, where very often one needs to reason about the size of a given data structure and not only about what its…
This paper proposes an evaluation of the adequacy of the constraint logic programming paradigm for natural language processing. Theoretical aspects of this question have been discussed in several works. We adopt here a pragmatic point of…
This paper proposes the use of Constraint Logic Programming (CLP) to model SQL queries in a data-independent abstract layer by focusing on some semantic properties for signalling possible errors in such queries. First, we define a…
Solving constraints involving inductive (aka recursive) definitions is challenging. State-of-the-art SMT/CHC solvers and first-order logic provers provide only limited support for solving such constraints, especially when they involve,…
The original CLIP text encoder is limited by a maximum input length of 77 tokens, which hampers its ability to effectively process long texts and perform fine-grained semantic understanding. In addition, the CLIP text encoder lacks support…
The CLP scheme uses Horn clauses and SLD resolution to generate multiple constraint satisfaction problems (CSPs). The possible CSPs include rational trees (giving Prolog) and numerical algorithms for solving linear equations and linear…
Constraint Logic Programming (CLP) is a language scheme for combining two declarative paradigms: constraint solving and logic programming. Concurrent Constraint Programming (CCP) is a declarative model for concurrency where agents interact…
Prolog is a well-known declarative programming language commonly used in introductory courses on logic and reasoning. However, many students find Prolog challenging because it lacks the familiar debugging mechanisms found in imperative…
Logic programming is a declarative programming paradigm. Programming language Prolog makes logic programming possible, at least to a substantial extent. However the Prolog debugger works solely in terms of the operational semantics. So it…
Slicing is a program analysis technique originally developed for imperative languages. It facilitates understanding of data flow and debugging. This paper discusses slicing of Constraint Logic Programs. Constraint Logic Programming (CLP) is…
The state-of-the-art in optimal control from timed temporal logic specifications, including Metric Temporal Logic (MTL) and Signal Temporal Logic (STL), is based on Mixed-Integer Convex Programming (MICP). The standard MICP approach is…
Concolic testing is a popular software verification technique based on a combination of concrete and symbolic execution. Its main focus is finding bugs and generating test cases with the aim of maximizing code coverage. A previous approach…
State-of-the-art SAT solvers are nowadays able to handle huge real-world instances. The key to this success is the so-called Conflict-Driven Clause-Learning (CDCL) scheme, which encompasses a number of techniques that exploit the conflicts…
Partial functions are common abstractions in formal specification notations such as Z, B and Alloy. Conversely, executable programming languages usually provide little or no support for them. In this paper we propose to add partial…
Large Language Models (LLMs) have upended decades of pedagogy in computing education. Students previously learned to code through \textit{writing} many small problems with less emphasis on code reading and comprehension. Recent research has…
Linear integer constraints are one of the most important constraints in combinatorial problems since they are commonly found in many practical applications. Typically, encodings to Boolean satisfiability (SAT) format of conjunctive normal…