scientific article

zbMath0646.68004MaRDI QIDQ4040341

Peter Padawitz

Publication date: 5 June 1993

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

denotational semanticsnarrowingrecursion theoryparamodulationChurch-Rosser propertysequent logicgoal reductionmany-sorted Horn logic with equality

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65) Classical first-order logic (03B10) Research exposition (monographs, survey articles) pertaining to computer science (68-02)

Related Items (30)

Generic induction proofs ⋮ An optimal narrowing strategy for general canonical systems ⋮ A proof system for conditional algebraic specifications ⋮ Knuth-bendix completion of horn clause programs for restricted linear resolution and paramodulation ⋮ Implicit induction in conditional theories ⋮ Functorial theory of parameterized specifications in a general specification framework ⋮ Completion-time optimization of rewrite-time goal solving ⋮ Detecting redundant narrowing derivations by the LSE-SL reducibility test ⋮ Incremental constraint satisfaction for equational logic programming ⋮ A Debugging Scheme for Functional Logic Programs1 1This work has been partially supported by CICYT under grant TIC2001-2705-C03-01, by Acción Integrada Hispano-Italiana HI2000-0161, Acción Integrada Hispano-Alemana HA2001-0059 and by Generalitat Valenciana under grant GV01-424. ⋮ An integrated framework for the diagnosis and correction of rule-based programs ⋮ Reasoning with conditional axioms ⋮ Logic programs with equational type specifications ⋮ Jungle rewriting: An abstract description of a lazy narrowing machine ⋮ Equivalence and difference between institutions: simulating Horn Clause Logic with based algebras ⋮ Three views on dependency covers from an FCA perspective ⋮ Conditional equational theories and complete sets of transformations ⋮ Horn clause programs with polymorphic types: Semantics and resolution ⋮ An Access Control Language Based on Term Rewriting and Description Logic ⋮ Proving semantical equivalence of data specifications ⋮ Functional Logic Programming: From Theory to Curry ⋮ Shallow confluence of conditional term rewriting systems ⋮ Mechanizable inductive proofs for a class of ∀ ∃ formulas ⋮ Conditional narrowing modulo a set of equations ⋮ A hybrid programming scheme combining fuzzy-logic and functional-logic resources ⋮ Swinging types=functions+relations+transition systems ⋮ Relating CASL with other specification languages: the institution level. ⋮ Expander2: Program Verification Between Interaction and Automation ⋮ Observational proofs by rewriting. ⋮ Contextual rewriting as a sound and complete proof method for conditional LOG-specifications

This page was built for publication: