• Maude

  • Referenced in 698 articles [sw06233]
  • system supporting both equational and rewriting logic specification and programming for a wide range ... equational logic sublanguage. Besides supporting equational specification and programming, Maude also supports rewriting logic computation...
  • OBJ3

  • Referenced in 140 articles [sw05370]
  • program specification and proof system based on order sorted equational logic. It has been successfully ... first language to implement parameterized programming and its module system influenced the designs...
  • OTTER

  • Referenced in 316 articles [sw02904]
  • prove theorems stated in first-order logic with equality. Otter’s inference rules are based ... symbolic calculator and has an embedded equational programming system. Otter is a fourth-generation Argonne ... research in abstract algebra and formal logic. Otter and its predecessors have been used...
  • Kiva-2

  • Referenced in 66 articles [sw08987]
  • This report documents the KIVA-2 computer program for the numerical calculation of transient ... ease-of-use. The KIVA-2 equations and numerical solution procedures are very general ... written for internal combustion engine calculations, the logic for these specifications can be easily modified ... KIVA-2 program, we describe in detail the equations solved, the numerical solution procedure...
  • EQP

  • Referenced in 12 articles [sw15620]
  • automated theorem proving program for first-order equational logic. Its strengths are good implementations...
  • UTP2

  • Referenced in 5 articles [sw06342]
  • support the higher-order logic, alphabets, equational reasoning and “programs as predicates” style that...
  • Saoithin

  • Referenced in 4 articles [sw06341]
  • support the higher-order logic, alphabets, equational reasoning and “programs as predicates” style that...
  • JPAX

  • Referenced in 30 articles [sw09906]
  • tool facilitates automated instrumentation of a program’s bytecode, which when executed will emit ... temporal logic verification, the deadlock analysis and the data race analysis. Temporal logic specifications ... rewriting system for equational logic, but here extended with executable temporal logic. The Maude rewriting ... event stream. JPAX can be used during program testing to gain increased information about program...
  • DDebugger

  • Referenced in 15 articles [sw09904]
  • Declarative debugging of rewriting logic specifications. Declarative debugging is a semi-automatic technique that starts ... from an incorrect computation and locates a program fragment responsible for the error by building ... find the error. Membership equational logic (MEL) is an equational logic that in addition...
  • CS-Prolog

  • Referenced in 7 articles [sw00171]
  • delay mechanism of the standard logic programming language is discussed. Capabilities of CS-PROLOG ... shown by example of solving linear arithmetic equations. CS-PROLOG uses four rules: variable elimination...
  • cheney-kincaid

  • Referenced in 25 articles [sw11656]
  • presumably they are most helpful. The computer programs in te book have been revised ... instead. The chapters have been reordered for logical and pedagogical reasons. The discussion of floating ... chapter on solving linear systems of equations. A new appendix on the concepts and notation...
  • ModuRes

  • Referenced in 4 articles [sw13122]
  • type systems or logics for reasoning about concurrent higher-order imperative programming languages ... solutions to certain kinds of recursive domain equations, which in practice has been a barrier ... provides an easy way to solve such equations. We show how the library ... type systems and logics for reasoning about concurrent higher-order imperative programming languages...
  • Zelus

  • Referenced in 4 articles [sw20166]
  • programming language for modeling systems that mix discrete logical time and continuous time behaviors. From ... with Ordinary Differential Equations (ODEs). The extension is conservative: any synchronous program expressed as data...
  • TILOS

  • Referenced in 8 articles [sw11680]
  • convex equations describing T are a particular class of functions called posynomials. Convex programs have ... certain to be globally optimal TILOS (Timed Logic Synthesizer) is a program that sizes transistors...
  • Z3-str

  • Referenced in 9 articles [sw19493]
  • Existing string solvers either ignore non-string program behavior or support limited set of string ... strings in terms of other primitives. The logic of the plug-in has three sorts ... over string terms. The atomic formulas are equations over string terms, and (in)-equalities over ... solver have features that enable whole program symbolic, static and dynamic analysis, but also...
  • Java+ITP

  • Referenced in 8 articles [sw32259]
  • equational theory in Maude. It supports compositional reasoning in a Hoare logic for this Java ... extensible and modular rewriting logic semantics of programming languages, for which CPS axiomatizations are indeed...
  • FLISP

  • Referenced in 4 articles [sw02536]
  • fuzzy data. The paper describes a new programming language (called FLISP) which provides a number ... based upon fuzzy sets and fuzzy logic theories. the language contains a collection of fuzzy ... operations and procedures for solution fuzzy relational equations with triangular norms. FLISP forms a plausible...
  • CFLP

  • Referenced in 5 articles [sw18674]
  • software system consisting of a functional logic programming interpreter running on one machine ... functional logic and involving constraints such as systems of linear, polynomial, differential equations, and equations...
  • Alpha

  • Referenced in 6 articles [sw13717]
  • level specification. An algorithm is described by equations involving variables defined on multi-dimensional domains ... Then, this description can be translated towards logic synthesis tools in order to generate ... polyhedra calculus, abstract and non-standard interpretation, program verification, optimization, architecture synthesis, VLSI, FPGA, systolic...
  • Newton

  • Referenced in 6 articles [sw21236]
  • reconcile the declarative nature of constraint logic programming (CLP) languages over intervals with advanced interval ... applications in science and engineering, including nonlinear equation-solving, unconstrained optimization, and constrained optimization...