Programming via Rewriting

Author

Câzãnescu, Virgil Emil

Author_Institution

Fac. of Math. & Comput. Sci., Univ. of Bucharest, Bucharest, Romania

fYear

2010

fDate

23-26 Sept. 2010

Firstpage

3

Lastpage

3

Abstract

Programming via rewriting is a part of the declarative programming which is illustrated by the languages: OBJ, Maude, CafeOBJ, CASL and so on. Programming via rewriting is very close to the equational logic. In the equational logic a set Γ of axioms is given. Axioms are Horn clauses, called also conditional equations. We are looking for all universal quantified equalities which are consequences of these axioms. Equational logic gives us a sound and complete set of deduction rules for these consequences: reflexivity, symmetry, transitivity, compatibility with operations and substitution. Programming via rewriting tries more: to find a proof for each consequence of these axioms. In a lot of cases such a proof may be found.

Keywords

Horn clauses; logic programming; probabilistic logic; rewriting systems; set theory; Horn clauses; axioms; conditional equations; declarative programming; deduction rules; equational logic; rewriting; Algebra; Computers; Equations; Mathematical model; Programming; Semantics;

fLanguage

English

Publisher

ieee

Conference_Titel

Symbolic and Numeric Algorithms for Scientific Computing (SYNASC), 2010 12th International Symposium on

Conference_Location

Timisoara

Print_ISBN

978-1-4244-9816-1

Type

conf

DOI

10.1109/SYNASC.2010.90

Filename

5715260