Category-based modularisation for equational logic programming
type: Item
instance of: scholarly article
title: Category-based modularisation for equational logic programming
zbMATH Open document ID: 0849.68012
author: Răzvan Diaconescu
published in: Acta Informatica
publication date: 1995-11-19T00:00:00Z
review text: Although modularisation is basic to modern computing, it has been little studied for logic-based programming. We treat modularisation for equational logic programming using the institution of category-based equational logic in three different ways: (1) to provide a generic satisfaction condition for equational logics; (2) to give a category-based semantics for queries and their solutions; and (3) as an abstract definition of compilation from one (equational) logic programming language to another. Regarding (2), we study soundness and completeness for equational logic programming queries and their solutions. This can be understood as ordinary soundness and completeness in a suitable ``non-logical'' institution. Soundness holds for all module imports, but completeness only holds for conservative module imports. Category-based equational signatures are seen as modules, and morphisms of such signatures as module imports. Regarding (3), completeness corresponds to compiler correctness. The results of this research applies to languages based on wide class of equational logic systems, including Horn clause logic, with or without equality; all variant of order and many sorted equational logic, including working modulo a set of axioms; constraint logic programming over arbitrary user-defined data types; and any combination of the above. Most importantly, due to the abstraction level, this research gives the possibility to have semantics and to study modularisation for equational logic programming developed over non-conventional structures.
reviewed by: Răzvan Diaconescu
Mathematics Subject Classification ID: 68N17
Mathematics Subject Classification ID: 68Q55
Mathematics Subject Classification ID: 18C10
Mathematics Subject Classification ID: 03B70
Mathematics Subject Classification ID: 68N20
zbMATH DE Number: 814158
zbMATH Keywords: modularisation
zbMATH Keywords: logic-based programming
zbMATH Keywords: category-based equational logic
zbMATH Keywords: category-based semantics
zbMATH Keywords: soundness
zbMATH Keywords: completeness
zbMATH Keywords: compiler correctness
describes a project that uses: OBJ3
MaRDI profile type: Publication
full work available at URL: s002360050054
OpenAlex ID: W2043675079
cites work: Q3950541
cites work: Axioms for abstract model theory
cites work: Q3714043
cites work: Q3906394
cites work: Q4284237
cites work: Computing with rewrite systems
cites work: Q4385532
cites work: Completeness of category-based equational deduction
cites work: Q3993363
cites work: Proving and rewriting
cites work: Q4723263
cites work: Institutions: abstract model theory for specification and programming
cites work: An Oxford survey of order sorted algebra
cites work: Q3737481
cites work: Q3716279
cites work: Q3030249
cites work: Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
cites work: Q4693062
cites work: Q4038704
cites work: Q5639839
cites work: Q3789064
cites work: Q3032225
cites work: Q3204056
cites work: A simple algebraic proof of the equational interpolation theorem
cites work: Q4725720
cites work: On observational equivalence and algebraic specification
cites work: Specifications in an arbitrary institution
cites work: The formal theory of monads
cites work: Q3776610
cites work: On the existence of free models in abstract algebraic institutions
cites work: Quasi-varieties in abstract algebraic institutions
DOI: 10.1007/S002360050054
description: scientific article; zbMATH DE number 814158