Adding partial functions to constraint logic programming with sets

DOI10.1017/S1471068415000290MaRDI QIDQ4593005zbMATH OpenOpenAlexWikidataFDO

Authors Maximiliano Cristiá, Gianfranco Rossi, Claudia Frydman

Publication date 9 November 2017

Published in Theory and Practice of Logic Programming (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1507.06852

zbMATH Keywords

logset theorypartial functionsCLP

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Logic programming (68N17) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: 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 functions as a primitive feature to a Constraint Logic Programming (CLP) language, namely {log}. Although partial functions could be programmed on top of {log}, providing them as first-class citizens adds valuable flexibility and generality to the form of set-theoretic formulas that the language can safely deal with. In particular, the paper shows how the {log} constraint solver is naturally extended in order to accommodate for the new primitive constraints dealing with partial functions. Efficiency of the new version is empirically assessed by running a number of non-trivial set-theoretical goals involving partial functions, obtained from specifications written in Z.

Recommendations

• Set constraints and logic programming
• Partial Functions and Equality in Answer Set Programming
• A first order logic for partial functions
• Reasoning about partial functions in the formal development of programs
• A set theory with support for partial functions

Cites work

• scientific article; zbMATH DE number 3976287 (Why is no real title available?)
• scientific article; zbMATH DE number 42431 (Why is no real title available?)
• scientific article; zbMATH DE number 2013571 (Why is no real title available?)
• Handbook of constraint programming.
• Interval propagation to reason about sets: Definition and implementation of a practical language
• The B-Book
• {log}: A language for programming in logic with finite sets

Cited in

(5)

• Solving quantifier-free first-order constraints over finite sets and binary relations
• scientific article; zbMATH DE number 7552283 (Why is no real title available?)
• A practical decision procedure for quantifier-free, decidable languages extended with restricted quantifiers
• Automated reasoning with restricted intensional sets
• Towards systematic treatment of partial functions in knowledge representation

Describes a project that uses

Uses Software

• SETL
• Z
• Alloy

This page was built for publication: Adding partial functions to constraint logic programming with sets

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4593005)