Inductive expansion: A calculus for verifying and synthesizing functional and logic programs

DOI10.1007/BF00249354zbMath0723.68074OpenAlexW2063221996MaRDI QIDQ757077

Peter Padawitz

Publication date: 1991

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf00249354

zbMATH Keywords

reductionconfluenceinductionresolutionalgebraic specificationHorn logicparamodulation

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Logic programming (68N17)

Related Items (2)

Generic induction proofs ⋮ Inductive theorem proving by consistency for first-order clauses

This page was built for publication: Inductive expansion: A calculus for verifying and synthesizing functional and logic programs