Mechanizing reasoning about large finite tables in a rewrite based theorem prover

Deepak Kapur, Mahadevan Subramaniam

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Finite tables are commonly used in many hardware and soft- ware applications. In most theorem provers, tables are typically axiomatized using predicates over the table indices. For proving conjectures expressed using such tables, provers often have to resort to brute force case analysis, usually based on indices of a table. Resulting proofs can be unnecessarily complicated and lengthy. They are often inefficient to generate as well as difficult to understand. Large tables are often man- ually abstracted using predicates, which is error-prone; furthermore, the correctness of abstractions must be ensured. An approach for modeling finite tables as a special data structure is proposed for use in Rewrite Rule Laboratory (RRL), a theorem prover for mechanizing equational reasoning and induction based on rewrite techniques. Dontcare entries in tables can be handled explicitly. This approach allows tables to be handled directly without having to resort to any abstraction mechanism. For efficiently processing large tables, concepts of a sparse and weakly sparse tables are introduced based on how frequently particular values appear as table entries. Sparsity in the tables is exploited in correctness proofs by doing case analyses on the table entries rather on the indices. The generated cases are used to deduce constraints on the table indices. Additional domain information about table indices can then be used to further simplify constraints on indices and check them. The methodology is illustrated using a nontrivial correctness proof of the hardware SRT division circuit performed in RRL. 1536 cases originally needed in the correctness proof are reduced to 12 top level cases by using the proposed approach. Each individual top level case generated is much simpler, even though it may have additional subcases. The proposed approach is likely to provide similar gains for applications such as hardware circuits for square root and other arithmetic functions, in which much larger and multiple lookup tables, having structure similar to the sparse structure of the SRT table, are used.

Original languageEnglish (US)
Title of host publicationAdvances in Computing Science ASIAN 1998 - 4th Asian Computing Science Conference, Proceedings
EditorsAtsushi Ohori, Jieh Hsiang
PublisherSpringer Verlag
Pages22-42
Number of pages21
ISBN (Print)3540653880, 9783540653882
StatePublished - Jan 1 1998
Event4th Asian Computing Science Conference, ASIAN 1998 - Manila, Philippines
Duration: Dec 8 1998Dec 10 1998

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume1538
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other4th Asian Computing Science Conference, ASIAN 1998
CountryPhilippines
CityManila
Period12/8/9812/10/98

Fingerprint

Tables
Reasoning
Hardware
Table lookup
Table
Networks (circuits)
Theorem
Application programs
Computer hardware
Data structures
Processing
Correctness
Predicate
Arithmetic Functions
Proof of correctness
Look-up Table
Sparsity
Square root
Deduce
Division

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Kapur, D., & Subramaniam, M. (1998). Mechanizing reasoning about large finite tables in a rewrite based theorem prover. In A. Ohori, & J. Hsiang (Eds.), Advances in Computing Science ASIAN 1998 - 4th Asian Computing Science Conference, Proceedings (pp. 22-42). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1538). Springer Verlag.

Mechanizing reasoning about large finite tables in a rewrite based theorem prover. / Kapur, Deepak; Subramaniam, Mahadevan.

Advances in Computing Science ASIAN 1998 - 4th Asian Computing Science Conference, Proceedings. ed. / Atsushi Ohori; Jieh Hsiang. Springer Verlag, 1998. p. 22-42 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1538).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Kapur, D & Subramaniam, M 1998, Mechanizing reasoning about large finite tables in a rewrite based theorem prover. in A Ohori & J Hsiang (eds), Advances in Computing Science ASIAN 1998 - 4th Asian Computing Science Conference, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 1538, Springer Verlag, pp. 22-42, 4th Asian Computing Science Conference, ASIAN 1998, Manila, Philippines, 12/8/98.
Kapur D, Subramaniam M. Mechanizing reasoning about large finite tables in a rewrite based theorem prover. In Ohori A, Hsiang J, editors, Advances in Computing Science ASIAN 1998 - 4th Asian Computing Science Conference, Proceedings. Springer Verlag. 1998. p. 22-42. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
Kapur, Deepak ; Subramaniam, Mahadevan. / Mechanizing reasoning about large finite tables in a rewrite based theorem prover. Advances in Computing Science ASIAN 1998 - 4th Asian Computing Science Conference, Proceedings. editor / Atsushi Ohori ; Jieh Hsiang. Springer Verlag, 1998. pp. 22-42 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{c57cf02e2fe7445e9adcc91b79c1b465,
title = "Mechanizing reasoning about large finite tables in a rewrite based theorem prover",
abstract = "Finite tables are commonly used in many hardware and soft- ware applications. In most theorem provers, tables are typically axiomatized using predicates over the table indices. For proving conjectures expressed using such tables, provers often have to resort to brute force case analysis, usually based on indices of a table. Resulting proofs can be unnecessarily complicated and lengthy. They are often inefficient to generate as well as difficult to understand. Large tables are often man- ually abstracted using predicates, which is error-prone; furthermore, the correctness of abstractions must be ensured. An approach for modeling finite tables as a special data structure is proposed for use in Rewrite Rule Laboratory (RRL), a theorem prover for mechanizing equational reasoning and induction based on rewrite techniques. Dontcare entries in tables can be handled explicitly. This approach allows tables to be handled directly without having to resort to any abstraction mechanism. For efficiently processing large tables, concepts of a sparse and weakly sparse tables are introduced based on how frequently particular values appear as table entries. Sparsity in the tables is exploited in correctness proofs by doing case analyses on the table entries rather on the indices. The generated cases are used to deduce constraints on the table indices. Additional domain information about table indices can then be used to further simplify constraints on indices and check them. The methodology is illustrated using a nontrivial correctness proof of the hardware SRT division circuit performed in RRL. 1536 cases originally needed in the correctness proof are reduced to 12 top level cases by using the proposed approach. Each individual top level case generated is much simpler, even though it may have additional subcases. The proposed approach is likely to provide similar gains for applications such as hardware circuits for square root and other arithmetic functions, in which much larger and multiple lookup tables, having structure similar to the sparse structure of the SRT table, are used.",
author = "Deepak Kapur and Mahadevan Subramaniam",
year = "1998",
month = "1",
day = "1",
language = "English (US)",
isbn = "3540653880",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "22--42",
editor = "Atsushi Ohori and Jieh Hsiang",
booktitle = "Advances in Computing Science ASIAN 1998 - 4th Asian Computing Science Conference, Proceedings",

}

TY - GEN

T1 - Mechanizing reasoning about large finite tables in a rewrite based theorem prover

AU - Kapur, Deepak

AU - Subramaniam, Mahadevan

PY - 1998/1/1

Y1 - 1998/1/1

N2 - Finite tables are commonly used in many hardware and soft- ware applications. In most theorem provers, tables are typically axiomatized using predicates over the table indices. For proving conjectures expressed using such tables, provers often have to resort to brute force case analysis, usually based on indices of a table. Resulting proofs can be unnecessarily complicated and lengthy. They are often inefficient to generate as well as difficult to understand. Large tables are often man- ually abstracted using predicates, which is error-prone; furthermore, the correctness of abstractions must be ensured. An approach for modeling finite tables as a special data structure is proposed for use in Rewrite Rule Laboratory (RRL), a theorem prover for mechanizing equational reasoning and induction based on rewrite techniques. Dontcare entries in tables can be handled explicitly. This approach allows tables to be handled directly without having to resort to any abstraction mechanism. For efficiently processing large tables, concepts of a sparse and weakly sparse tables are introduced based on how frequently particular values appear as table entries. Sparsity in the tables is exploited in correctness proofs by doing case analyses on the table entries rather on the indices. The generated cases are used to deduce constraints on the table indices. Additional domain information about table indices can then be used to further simplify constraints on indices and check them. The methodology is illustrated using a nontrivial correctness proof of the hardware SRT division circuit performed in RRL. 1536 cases originally needed in the correctness proof are reduced to 12 top level cases by using the proposed approach. Each individual top level case generated is much simpler, even though it may have additional subcases. The proposed approach is likely to provide similar gains for applications such as hardware circuits for square root and other arithmetic functions, in which much larger and multiple lookup tables, having structure similar to the sparse structure of the SRT table, are used.

AB - Finite tables are commonly used in many hardware and soft- ware applications. In most theorem provers, tables are typically axiomatized using predicates over the table indices. For proving conjectures expressed using such tables, provers often have to resort to brute force case analysis, usually based on indices of a table. Resulting proofs can be unnecessarily complicated and lengthy. They are often inefficient to generate as well as difficult to understand. Large tables are often man- ually abstracted using predicates, which is error-prone; furthermore, the correctness of abstractions must be ensured. An approach for modeling finite tables as a special data structure is proposed for use in Rewrite Rule Laboratory (RRL), a theorem prover for mechanizing equational reasoning and induction based on rewrite techniques. Dontcare entries in tables can be handled explicitly. This approach allows tables to be handled directly without having to resort to any abstraction mechanism. For efficiently processing large tables, concepts of a sparse and weakly sparse tables are introduced based on how frequently particular values appear as table entries. Sparsity in the tables is exploited in correctness proofs by doing case analyses on the table entries rather on the indices. The generated cases are used to deduce constraints on the table indices. Additional domain information about table indices can then be used to further simplify constraints on indices and check them. The methodology is illustrated using a nontrivial correctness proof of the hardware SRT division circuit performed in RRL. 1536 cases originally needed in the correctness proof are reduced to 12 top level cases by using the proposed approach. Each individual top level case generated is much simpler, even though it may have additional subcases. The proposed approach is likely to provide similar gains for applications such as hardware circuits for square root and other arithmetic functions, in which much larger and multiple lookup tables, having structure similar to the sparse structure of the SRT table, are used.

UR - http://www.scopus.com/inward/record.url?scp=84947943679&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84947943679&partnerID=8YFLogxK

M3 - Conference contribution

SN - 3540653880

SN - 9783540653882

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 22

EP - 42

BT - Advances in Computing Science ASIAN 1998 - 4th Asian Computing Science Conference, Proceedings

A2 - Ohori, Atsushi

A2 - Hsiang, Jieh

PB - Springer Verlag

ER -