The effective integration of decision procedures in formula simplification is a fundamental problem in mechanical verification. The main source of difficulty occurs when the decision procedure is asked to solve goals containing symbols which are interpreted for the prover but uninterpreted for the decision procedure. To cope with the problem, Boyer & Moore proposed a technique, called augmentation, which extends the information available to the decision procedure with suitably selected facts. Constraint Contextual Rewriting (CCR, for short) is an extended form of contextual rewriting which generalizes the Boyer & Moore integration schema. In this paper we give a detailed account of the control issues related to the termination of CCR. These are particularly subtle and complicated since augmentation is mutually dependent from rewriting and it must be prevented from indefinitely extending the set of facts available to the decision procedure. A proof of termination of CCR is given.

Termination of constraint contextual rewriting / Armando, A.; Ranise, S.. - 1794:(2000), pp. 47-61. (Intervento presentato al convegno 3rd International Workshop on Frontiers of Combining Systems, FroCoS 2000 tenutosi a fra nel 2000) [10.1007/10720084_4].

Termination of constraint contextual rewriting

Ranise S.
2000-01-01

Abstract

The effective integration of decision procedures in formula simplification is a fundamental problem in mechanical verification. The main source of difficulty occurs when the decision procedure is asked to solve goals containing symbols which are interpreted for the prover but uninterpreted for the decision procedure. To cope with the problem, Boyer & Moore proposed a technique, called augmentation, which extends the information available to the decision procedure with suitably selected facts. Constraint Contextual Rewriting (CCR, for short) is an extended form of contextual rewriting which generalizes the Boyer & Moore integration schema. In this paper we give a detailed account of the control issues related to the termination of CCR. These are particularly subtle and complicated since augmentation is mutually dependent from rewriting and it must be prevented from indefinitely extending the set of facts available to the decision procedure. A proof of termination of CCR is given.
2000
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Germany
Springer Verlag
978-3-540-67281-4
978-3-540-46421-1
Armando, A.; Ranise, S.
Termination of constraint contextual rewriting / Armando, A.; Ranise, S.. - 1794:(2000), pp. 47-61. (Intervento presentato al convegno 3rd International Workshop on Frontiers of Combining Systems, FroCoS 2000 tenutosi a fra nel 2000) [10.1007/10720084_4].
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11572/333296
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 9
  • ???jsp.display-item.citation.isi??? ND
social impact