scientific article
From MaRDI portal
Publication:4040341
zbMath0646.68004MaRDI QIDQ4040341
Publication date: 5 June 1993
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
denotational semanticsnarrowingrecursion theoryparamodulationChurch-Rosser propertysequent logicgoal reductionmany-sorted Horn logic with equality
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
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
