Expresso is a Java library developed at SRI International's Artificial Intelligence Center for representing and evaluating symbolic expressions in Java. The representation portion of Expresso concentrates on:
- Representation of expressions (boolean formulas, arithmetic, sets, and function applications).
- Parsing human readable strings into expressions and back again.
grinder. Its base algorithm is called Symbolic Generic DPLL Modulo Theories (SGDPLL(T)), detailed in the paper
"Probabilistic Inference Modulo Theories",
de Salvo Braz, R., O'Reilly, C., Gogate, V., Dechter, R.,
Proc. of the 25th International Joint Conference on Artificial Intelligence (IJCAI-16).
(revised version, original version, bibtex)
- propositional variables
- equality on categorical types
- equality and inequalities over bounded integers (more specifically, difference arithmetic).
- linear real arithmetic
- algebraic data types
- uninterpreted functions
Your possible next steps:
- Play with the symbolic shell demo (requires a browser that supports Java Web Start. You also need to whitelist http://aic-sri-international.github.io and authorize applications to run from the browser in the Java Control Panel, which in Windows is an icon in the Control Panel, and in other platforms is a separate application)
- Use the library through Maven in your own JVM projects (see "Latest Maven information" at "Getting Started")
- Install the project to use in your own JVM projects or become a contributor