Adding partial functions to Constraint Logic Programming with sets

DOI10.1017/S1471068415000290zbMATH Open1379.68053arXiv1507.06852OpenAlexW3103318063WikidataQ57840329 ScholiaQ57840329MaRDI QIDQ4593005FDOQ4593005

Claudia Frydman, Maximiliano Cristiá, Gianfranco Rossi

Publication date: 9 November 2017

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

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.

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)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• The B-Book
• {log}: A language for programming in logic with finite sets
• Interval propagation to reason about sets: Definition and implementation of a practical language
• Title not available (Why is that?)

Cited In (5)

• Solving quantifier-free first-order constraints over finite sets and binary relations
• Title not available (Why is that?)
• 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

Uses Software

• Alloy
• Z
• SETL

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)