Home Page

The {log} (read setlog) project aims at the design and development of a Constraint Logic Programming language that embodies the fundamental forms of set designation and a number of primitive operations for set management.
Various new features have been added to the core part of the language since the initial development of {log}. Among them, basic facilities for representing and manipulating intervals (integrating the CLP(FD) solver), binary relations, partial functions, Cartesian products and restricted intensional sets.
The {log} language can be used either as a stand-alone CLP language or as an addition to Prolog that allows to extend Prolog with set constraint management facilities. 

Using {log}

• The {log} interpreter
{log} Version 4.9.8 Release 14i (last update, March 2024)
refer to this paper for a general presentation of the first version of {log}.


• {log} library files (save them into the same directory as 'setlog.pl')
• setloglib.slog {log} standard library - provides basic set-theoretic operations that are not supplied as constraints by the language
• setloglibpf.slog provides basic operations on partial functions that are not supplied as constraints by the language
• setloglibTPTP.slog provides operations on sets, binary relations and partial functions that are useful for dealing with problems from the TPTP library
• setlogliblist.slog provides basic operations on lists, represented as sets (following the standard definitions given in the Z mathematical toolkit regarding lists)
• setloglib_tc.slog provides a typed version of general operations on sets, binary relations and integer intervals


• Programming examples
• A gallery of simple {log} programs
• The N Queens Problem
• Traveling Salesman Problem
• Map coloring (using set constraints only) (using FD constraints)
• The SEND + MORE = MONEY puzzle
• Find paths in a directed weighted graph
• Training a weighted automata
• A naive interpreter for the GAMMA language (with applications) (using sets) (using multisets)


• Applications
• Implementing P systems for membrane computing (paper) (program)
• Using {log} as a test case generator for the Test Template Framework (paper) (programs using Version 4.8.0)
• Automated proof of Bell-LaPadula security properties (paper) (programs) (programs - alternative model)
• Implementing the Tokeneer ID Station Specification (paper) (programs)
• An automatically verified prototype of a Landing Gear System (programs)
• An automatically verified prototype of Android permissions system. Translation into {log} of a Coq model (programs)
• Specifying and verifying state machines: the specification of the birthday book problem (the {log} forgram) ('forgram' is a portmanteau word resulting from the combination of 'formula' and 'program')


• Empirical evaluations
• An empirical evaluation for "A Decision Procedure for Sets, Binary Relations and Partial Functions", CAV (1) 2016 ({log} version 4.9.1-20): a document describing the evaluation; experimental data
• An empirical evaluation for "A Set Solver for Finite Set Relation Algebra", RAMiCS 2018 ({log} version 4.9.5-23): experimental data
• An empirical evaluation for "Solving Quantifier-Free First-Order Constraints Over Finite Sets and Binary Relations", JAR, v.64, no.2, 2020 ({log} version 4.9.5-19): experimental data
• An empirical evaluation for "Integrating Cardinality Constraints into Constraint Logic Programming with Sets", submitted, January 2021 ({log} version 4.9.8-7): experimental data
• An empirical evaluation for "A Decision Procedure for a Theory of Finite Sets with Finite Integer Intervals", submitted, May 2021 ({log} version 4.9.8-9): experimental data

• The {log} user manual ({log} Version 4.9.8 Release 14i)


• Rewrite Rules for {log}'s Set Solver (abstract definition)


• Two documents aimed at showing how Z/B specifications can be translated into {log} and how {log} can be used to run simulations and automated proofs: {log} Applications to Software Specification and Verification, From B Specifications to {log} Forgrams


• Main papers related to {log}


• Recent papers
1. Maximiliano Cristiá, Gianfranco Rossi:
   Automated proof of Bell-LaPadula security properties.
   Journal of Automated Reasoning.
   Volume 65, Number 4, 463-478 (2021). doi: 10.1007/s10817-020-09577-6. URL
2. Maximiliano Cristiá, Gianfranco Rossi:
   Solving Quantifier-Free First-Order Constraints Over Finite Sets and Binary Relations.
   Journal of Automated Reasoning.
   Volume 64, Number 2, 295-330 (2020)
3. Maximiliano Cristiá, Gianfranco Rossi:
   A Set Solver for Finite Set Relation Algebra.
   RAMiCS 2018: 333-349
4. Maximiliano Cristiá, Gianfranco Rossi:
   A Decision Procedure for Restricted Intensional Sets.
   CADE 2017: 185-201
5. Maximiliano Cristiá, Gianfranco Rossi:
   A Decision Procedure for Sets, Binary Relations and Partial Functions.
   CAV (1) 2016: 179-198
6. Maximiliano Cristiá, Gianfranco Rossi, Claudia S. Frydman:
   Adding partial functions to Constraint Logic Programming with sets.
   TPLP 15(4-5): 651-665 (2015)
7. Maximiliano Cristiá, Gianfranco Rossi, Claudia S. Frydman:
   {log} as a Test Case Generator for the Test Template Framework.
   SEFM 2013: 229-243


• Other papers

 

People



• Current developers
• Maximiliano Cristiá, Universidad Nacional de Rosario and French Argentine International Center for Information Systems and Sciences, Rosario (Argentina)
• Gianfranco Rossi, Università di Parma, Parma (Italy)


• Original developers
• Agostino Dovier
• Eugenio Omodeo
• Enrico Pontelli
• Gianfranco Rossi