AutStr: computing with infinite structures#
AutStr represents infinite mathematical structures as finite automata and lets you query them with first-order and monadic second-order logic. Start with the Overview for a guided tour; the showcase notebooks — executed freshly on every documentation build — work through each area in depth, and the API reference is generated from the docstrings.
Guide
- Overview
- Decision procedure and theorem prover
- Symbolic expressions instead of formula strings
- Computer algebra over infinite domains
- Uniformly automatic classes: one automaton for a whole family
- Composing presentations
- Defining one structure inside another
- Infinite graphs, and where first-order logic stops
- Bounded rank-width: groups and graphs from one linear algebra
- Implicit evaluation: members whose automata cannot be built
- How it works
Notebooks
- Arithmetic and algebra over infinite structures
- Infinite graphs, and how far first-order logic reaches
- Graphs of bounded width as uniformly automatic classes
- Groups as uniformly automatic classes
- Building new structures from old
- Implicit evaluation: querying members whose automata are too big to build
API reference
Project