Extensions of Logic Programming in Maude

By Santiago Escobar, VRAIN, Universitat Politècnica de València, Spain

In 2022/2023, the logic programming community is celebrating the milestone of 50 years of evolution of logic programming languages, started in 1972 with the first version of Prolog. In this paper, we consider how extensions of logic programming can be handled in Maude. Maude is a recently developed high-level programming language and system that supports functional, concurrent, logic, and object-oriented computations. A Maude rewrite theory R = (Σ, G, R) combines a set R of term rewrite rules, which specify the concurrent transitions of a system, with an equational theory G that specifies the algebraic datatypes of the system’s states.  G is split into a set E of equations and a set B of axioms. The axioms B are equalities representing algebraic laws such as associativity (A), commutativity (C), and unit symbols (U). The equations E are implicitly oriented from left to right as rewrite rules and operationally used as simplification rules modulo the axioms B. The rewrite rules R are applied to terms by  modulo the equations E and the axioms B.

The complete contribution can be read as PDF File: