scholarly journals Reflection in membership equational logic, many-sorted equational logic, Horn logic with equality, and rewriting logic

2007 ◽  
Vol 373 (1-2) ◽  
pp. 70-91 ◽  
Author(s):  
Manuel Clavel ◽  
José Meseguer ◽  
Miguel Palomino
Keyword(s):  
Equational Logic ◽  
Rewriting Logic ◽  
Horn Logic ◽  
Membership Equational Logic

MODULARITY AND CORRECTNESS FOR LOGIC PROGRAMS AND KNOWLEDGE BASES

1994 ◽  
Vol 04 (02) ◽  
pp. 257-275
Author(s):  
GRIGORIS ANTONIOU
Keyword(s):  
Logic Programming ◽  
Programming Languages ◽  
Formal Semantics ◽  
Knowledge Bases ◽  
Algebraic Specification ◽  
Equational Logic ◽  
Logic Programs ◽  
Horn Logic ◽  
Large Systems ◽  
The One

A modularity concept for structuring and developing large logic programs and logical knowledge bases is presented. The concept is motivated from work in the field of algebraic specification, and enforces an extreme modularity discipline that goes beyond the one found in imperative or logic programming languages. As concrete programming languages (respectively knowledge representation formalisms), we consider Horn logic and equational logic programming. We give formal semantics for single modules and discuss correctness and verification issues. Large systems are constructed as interconnections of single modules. We introduce the so-called module operations of composition, actualization, and union, and give results concerning compositionality of semantics and correctness preservation.

scholarly journals A Comparison of Petri Net Semantics under the Collective Token Philosophy

1998 ◽  
Vol 5 (17) ◽  
Author(s):  
Roberto Bruni ◽  
José Meseguer ◽  
Ugo Montanari ◽  
Vladimiro Sassone
Keyword(s):  
Petri Nets ◽  
Petri Net ◽  
Equational Logic ◽  
Monoidal Categories ◽  
Transition Systems ◽  
Logical Description ◽  
Membership Equational Logic

In recent years, several semantics for place/transition Petri nets have been proposed that adopt the collective token philosophy. We investigate distinctions and similarities between three such models, namely configuration structures, concurrent transition systems, and (strictly) symmetric (strict) monoidal categories. We use the notion of adjunction to express each connection. We also present a purely logical description of the collective token interpretation of net behaviours in terms of theories and theory morphisms in partial membership equational logic.

scholarly journals Declarative Debugging of Membership Equational Logic Specifications

2008 ◽  
pp. 174-193 ◽  
Author(s):  
Rafael Caballero ◽  
Narciso Martí-Oliet ◽  
Adrián Riesco ◽  
Alberto Verdejo
Keyword(s):  
Equational Logic ◽  
Membership Equational Logic

scholarly journals Specification and proof in membership equational logic

2000 ◽  
Vol 236 (1-2) ◽  
pp. 35-132 ◽  
Author(s):  
Adel Bouhoula ◽  
Jean-Pierre Jouannaud ◽  
José Meseguer
Keyword(s):  
Equational Logic ◽  
Membership Equational Logic

scholarly journals Logical Specification of Operational Semantics

1999 ◽  
Vol 6 (55) ◽  
Author(s):  
Peter D. Mosses
Keyword(s):  
Programming Languages ◽  
Operational Semantics ◽  
Rewriting Logic ◽  
Horn Logic ◽  
Semantics Of Programming Languages ◽  
Crucial Feature ◽  
Logical Specification ◽  
Inference Systems ◽  
Equational Specifications ◽  
The Relationship

Various logic-based frameworks have been proposed for <br />specifying the operational semantics of programming languages and <br />concurrent systems, including inference systems in the styles advocated by<br />Plotkin and by Kahn, Horn logic, equational specifications, reduction<br />systems for evaluation contexts, rewriting logic, and tile logic.<br />We consider the relationship between these frameworks, and assess their<br />respective merits and drawbacks - especially with regard to the modularity<br /> of specifications, which is a crucial feature for scaling up to practical<br />applications. We also report on recent work towards the use of the Maude<br />system (which provides an efficient implementation of rewriting logic) as<br />a meta-tool for operational semantics.

Flat algebras and the translation of universal Horn logic to equational logic

2008 ◽  
Vol 73 (1) ◽  
pp. 90-128 ◽  
Author(s):  
Marcel Jackson
Keyword(s):  
Finite Basis ◽  
Equational Logic ◽  
Subdirectly Irreducible ◽  
Horn Logic ◽  
Finite Algebras ◽  
Partial Structures ◽  
Partial Algebras ◽  
Fixed Type ◽  
Bottom Element ◽  
Definable Principal Congruences

AbstractWe describe which subdirectly irreducible flat algebras arise in the variety generated by an arbitrary class of flat algebras with absorbing bottom element. This is used to give an elementary translation of the universal Horn logic of algebras, partial algebras, and more generally still, partial structures into the equational logic of conventional algebras. A number of examples and corollaries follow. For example, the problem of deciding which finite algebras of some fixed type have a finite basis for their quasi-identities is shown to be equivalent to the finite identity basis problem for the finite members of a finiteiy based variety with definable principal congruences.

Sign in / Sign up

Export Citation Format

Share Document