Issue No. 01 - January (1989 vol. 15)

ISSN: 0098-5589

pp: 1-9

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/32.21720

ABSTRACT

<p>Significant modifications of the first-order rules have been developed so that they can be applied directly to algebraic expressions. The importance and implication of normalization of formulas in any theorem prover are discussed. It is shown how the properties of the domain of discourse have been taken care of either by the normalizer or by the inference rules proposed. Using a nontrivial example, the following capabilities of the verifier that would use these inference rules are highlighted: (1) closeness of the proof construction process to the human thought process; and (2) efficient handling of user provided axioms. Such capabilities make interfacing with humans easy.</p>

INDEX TERMS

inference rules; integer arithmetic; verification; flowchart programs; first-order rules; algebraic expressions; theorem prover; proof construction process; human thought process; user provided axioms; inference mechanisms; program verification; theorem proving.

CITATION

D.C. Sarkar, S.C. De Sarkar, "Some Inference Rules for Integer Arithmetic for Verification of Flowchart Programs on Integers",

*IEEE Transactions on Software Engineering*, vol. 15, no. , pp. 1-9, January 1989, doi:10.1109/32.21720