Skip to Main content Skip to Navigation
Conference papers

Applying semantic subsumption rules in the context of inductive proofs

Sorin Stratulat 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Due to the inherent incompleteness of the inductive proof methods, they should be combined with other methods more suitable to reason on specific domains. In the paper, it is shown how the standard inference system of SPIKE theorem prover can be extended with semantic subsumption rules in order to facilitate a better integration of other reasoning modules.
Document type :
Conference papers
Complete list of metadata

https://hal.inria.fr/inria-00098496
Contributor : Publications Loria <>
Submitted on : Monday, September 25, 2006 - 5:02:04 PM
Last modification on : Friday, February 26, 2021 - 3:28:06 PM

Identifiers

  • HAL Id : inria-00098496, version 1

Collections

Citation

Sorin Stratulat. Applying semantic subsumption rules in the context of inductive proofs. Workshop on Integration of Deductive Systems - CADE-15, 1998, none, 11 p. ⟨inria-00098496⟩

Share

Metrics

Record views

102