Name
Abstract | ||
|---|---|---|
Kapur and Subramaniam [8] defined syntactical classes of equations where inductive validity is decidable. Thus, their validity can be checked without any user interaction and hence, this allows an integration of (a restricted form of) induction in fully automated reasoning tools such as model checkers. However, the results of [8] were only restricted to equations. This paper extends the classes of conjectures considered in [8] to a larger class of arbitrary quantifier-free formulas (e.g., conjectures also containing negation, conjunction, disjunction, etc.). |
Year | DOI | Venue |
|---|---|---|
2001 | 10.1007/3-540-45744-5_41 | IJCAR |
Keywords | Field | DocType |
model checker,restricted form,inductive validity,larger class,decidable classes,automated reasoning tool,arbitrary quantifier-free formula,inductive theorems,user interaction,syntactical class | Discrete mathematics,Inductive reasoning,Automated reasoning,Negation,Computer science,Automated theorem proving,Algorithm,Decidability | Conference |
ISBN | Citations | PageRank |
3-540-42254-4 | 12 | 0.66 |
References | Authors | |
10 | 2 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Jürgen Giesl | 1 | 2048 | 124.90 |
| Deepak Kapur | 2 | 2282 | 235.00 |