Application of conditional term substitution systems in program verification (Q1091795)
From MaRDI portal
| This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use this page instead for the normal view: Application of conditional term substitution systems in program verification |
scientific article; zbMATH DE number 4011899
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | Application of conditional term substitution systems in program verification |
scientific article; zbMATH DE number 4011899 |
Statements
Application of conditional term substitution systems in program verification (English)
0 references
1986
0 references
We consider a class of theories intended to be used for program verification: they are close to Horn theories, but their expressive power is increased by allowing formulas of decidable subtheories in the axiom premises. A decision procedure is described which converts the axioms into conditional reduction rules and builds in the subtheory decision algorithms.
0 references
program verification
0 references
Horn theories
0 references
decidable subtheories
0 references
axiom premises
0 references
decision procedure
0 references
conditional reduction rules
0 references
0.7463415861129761
0 references