Name
Abstract | ||
|---|---|---|
In this paper we present an investigation into whether and how decision procedures can be learnt and built automatically. Our approach consists of two stages. First, a refined brute-force search procedure applies exhaustively a set of given elementary methods to try to solve a corpus of conjectures generated by a stochastic context-free grammar. The successful proof traces are saved. In the second stage, a learning algorithm (by Jamnik et al.) tries to extract a required supermethod (i.e., decision procedure) from the given traces. In the paper, this technique is applied to elementary methods that encode the operations of the Fourier-Motzkin's decision procedure for Presburger arithmetic on rational numbers. The results of our experiment are encouraging. |
Year | DOI | Venue |
|---|---|---|
2003 | 10.1016/S1571-0661(04)80662-5 | Electronic Notes in Theoretical Computer Science |
Keywords | Field | DocType |
stochastic context free grammar,presburger arithmetic,rational number | Discrete mathematics,ENCODE,Rational number,Computer science,Search procedure,Grammar,Presburger arithmetic,Theoretical computer science | Journal |
Volume | Issue | ISSN |
86 | 1 | 1571-0661 |
Citations | PageRank | References |
0 | 0.34 | 9 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Mateja Jamnik | 1 | 158 | 30.79 |
| Predrag Janičić | 2 | 130 | 12.27 |