./wip/mona, Tool that translates formulas to finite-state automata

[ CVSweb ] [ Homepage ] [ RSS ] [ Required by ] [ Add to tracker ]

Branch: CURRENT, Version: 18, Package name: mona-1.4-18, Maintainer: kamelderouiche

MONA implements decision procedures for the Weak Second-order Theory
of One or Two successors (WS1S/WS2S). The theory of one successor,
known as WS1S, is a fragment of arithmetic augmented with second-order
quantification over finite sets of natural numbers. Its first-order terms
denote just natural numbers. The theory has no addition, since that would
make it undecidable, but it has a unary operation +1, known as the successo
r function. WS2S is a generalization to tree structures. Since the theories are
monadic second-order logics, we call our tool MONA


Required to build:
[pkgtools/cwrappers]

Master sites:

Filesize: 686.632 KB

Version history: (Expand)