Yarralumla -
Yet Another Range Restriction Avoiding Loops Under Much Less Assumptions

Yarralumla is also a beautiful suburb in Canberra, ACT, Australia.

Yarralumla implements various transformations on clause logic formulas for the purpose of applying first-order bottom-up model generation (BUMG) systems. The transformations are thought to be useful to compute (finite) models, not to find refutations.

See the paper Improved Bottom-Up Model Generation by Peter Baumgartner and Renate Schmidt for a description of the transformations and the theory behind.

For meaningful operation one needs at the back-end a BUMG system. We experimented with two such systems, KRHyper and MSPASS.

Download and Further links

• README file with further information.
• Download the Yarralumla program: yarralumla.tar.gz
• The KRHyper system
• Regarding obtaining (a slightly modified, as is needed) version of MSPASS please contact Peter Baumgartner.
• Some helper scripts that make Yarralumla much easier to use: tme2dfg (rename it to tme2dfg.pl !), MSPASS-yarralumla-run, krhyper-yarralumla-run. See the README file for more information.

In case of questions or suggestions please contact Peter Baumgartner. Any feedback will be appreciated.

Thanks

Some library code for input/output is taken from Christoph Wernhard's KRHyper distribution.