Name
Abstract | ||
|---|---|---|
In this note, we describe how a fragment of arithmetic can be decided in practice. We follow essentially the ideas of [8], which we have embedded in the Mona tool. Mona is an implementation of Monadic Second-order Logic on finite strings (and trees). The previous semantics used in Mona is the one provided in current literature [7, 9], where the meaning of first-order terms is restricted to being a position in the string over which the formula is interpreted. In this note, we describe our new... |
Year | DOI | Venue |
|---|---|---|
1996 | 10.1007/3-540-61648-9_56 | FTRTFT |
Keywords | Field | DocType |
decidable arithmetic,first order | Algebra,Existential quantification,Hoare logic,Arithmetic,Finite-state machine,Decidability,Monadic predicate calculus,Mathematics | Conference |
Volume | ISSN | ISBN |
1135 | 0302-9743 | 3-540-61648-9 |
Citations | PageRank | References |
8 | 0.92 | 6 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Morten Biehl | 1 | 33 | 2.89 |
| Nils Klarlund | 2 | 645 | 65.43 |
| Theis Rauhe | 3 | 661 | 35.11 |