scientific article; zbMATH DE number 193539

MaRDI QIDQ4040341zbMATHFDO

Authors Peter Padawitz

Publication date 5 June 1993

zbMATH Keywords

denotational semanticsrecursion theorynarrowingparamodulationChurch-Rosser propertysequent logicgoal reductionmany-sorted Horn logic with equality

Mathematics Subject Classification ID

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

Recommendations

• Semantical and computational aspects of Horn approximations
• scientific article; zbMATH DE number 4085614
• Computing intersections of Horn theories for reasoning with models
• Publication:4205083
• Semantics of Horn and disjunctive logic programs
• scientific article; zbMATH DE number 2090546
• scientific article; zbMATH DE number 4160108
• Automated Deduction – CADE-20
• Deterministic and nondeterministic computation, and horn programs, on abstract data types
• Publication:4720780

Cited in

(35)

• Implicit induction in conditional theories
• Reasoning with conditional axioms
• Three views on dependency covers from an FCA perspective
• scientific article; zbMATH DE number 4125019 (Why is no real title available?)
• Conditional equational theories and complete sets of transformations
• Contextual rewriting as a sound and complete proof method for conditional LOG-specifications
• Incremental constraint satisfaction for equational logic programming
• Shallow confluence of conditional term rewriting systems
• Generic induction proofs
• Completion-time optimization of rewrite-time goal solving
• Conditional narrowing modulo a set of equations
• A proof system for conditional algebraic specifications
• Operational semantics of resolution and productivity in Horn clause logic
• Smallest horn clause programs
• An access control language based on term rewriting and description logic
• Equivalence and difference between institutions: simulating Horn Clause Logic with based algebras
• Proving semantical equivalence of data specifications
• Jungle rewriting: an abstract description of a lazy narrowing machine
• scientific article; zbMATH DE number 2090546 (Why is no real title available?)
• An integrated framework for the diagnosis and correction of rule-based programs
• Functional Logic Programming: From Theory to Curry
• Deterministic and nondeterministic computation, and horn programs, on abstract data types
• Functorial theory of parameterized specifications in a general specification framework
• Detecting redundant narrowing derivations by the LSE-SL reducibility test
• A hybrid programming scheme combining fuzzy-logic and functional-logic resources
• Mechanizable inductive proofs for a class of \(\forall \exists\) formulas
• Knuth-bendix completion of horn clause programs for restricted linear resolution and paramodulation
• Swinging types=functions+relations+transition systems
• Expander2: program verification between interaction and automation
• A debugging scheme for functional logic programs
• Horn clause programs with polymorphic types: Semantics and resolution
• An optimal narrowing strategy for general canonical systems
• Observational proofs by rewriting.
• Relating CASL with other specification languages: the institution level.
• Logic programs with equational type specifications

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4040341)