Finite Countermodel Machine
Jump to navigation
Jump to search
| Paradigm(s) | declarative, logic |
|---|---|
| Designed by | User:Ukeharu |
| Appeared in | 2025 |
| Memory system | State-based |
| Dimensions | one-dimensional |
| Computational class | Finite state automata |
| Reference implementation | Unimplemented |
| File extension(s) | .fcm |
- This is still a work in progress. It may be changed in the future.
Finite Countermodel Machine is an esoteric language designed by User:Ukeharu in 2025, based on relational models of modal logic and tableaux derivations. The language makes use of proof searching with tableaux to generate finite state automata that then run on a string given either at run-time or compile-time. The language requires both an understanding of proof theory and modal logics if one wishes to avoid intractable proof searches, which combined with the complexity of visualising how the premises of the tableaux proof relate to the final output, makes the language non-trivial to use without background knowledge.