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
  • Computer algebra over infinite domains
  • Uniformly automatic classes: one automaton for a whole family
  • Composing presentations
  • 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
• Graphs of bounded width as uniformly automatic classes
• Groups as uniformly automatic classes
• Composing presentations
• Implicit evaluation: querying members whose automata are too big to build

API reference

• autstr
  • autstr package

Indices and tables

• Index

• Module Index

• Search Page