Welcome to the guides index. Most people should start with the first chapter and work your way through, but if you know what you're doing, feel free to jump straight into the later chapters!
First Things First
- Welcome - Puzzle example. Aim of this site. Why it's worth doing.
- Introduction - A very simple example. Typing in a problem. Running the solver.
- More Introduction - Variations on the example. Multiple solutions and no solution.
- And More... - A more interesting example: the eight queens puzzle.
- And Yet More... - An even more interesting example: designing a meeting schedule.
Next Things Next
- Sorts - Sort declarations. Enumerated sorts. Cardinality-range sorts.
- Vocabulary - Declaring functions. Arity. Function types.
- Constraints - Basic syntax. Variables and constants.
- At Last: A Puzzle! - The Four Spies puzzle.
- A Harder Puzzle - The Inconsequential Seminars.
- Example of a theory - The girl with the diminutive ruminant
More Advanced Topics
- Built Ins - Sorts int and bool. Functions +, -, DIF, EST, =, <, >, NOT, AND, OR, IMP..
- Vocabulary Revisited - Function descriptions. Special kinds of function.
- Logical notation: Connectives - Propositional logical notation
- Logical notation: Quantifiers - First order logical notation.
- How many Romans? - How to say "one", "more than one", "three", etc.
- Existence - Use of partial functions and the "EST" predicate.
- Using EST: The Queens Again... - Illustrating use of the existence predicate and built-ins.
- Common Knowledge - Identifying unstated assumptions and making background knowledge explicit
- Return To The Railway - Illustrating the use of boolean operations, compound formulae and identity.
Really Advanced Topics
- Clause Form - General clauses. Multiple premises, multiple conclusions.
- More About Clauses - Expressing generality with free variables and Skolem functions
- Yet More About Clauses - Reduction to clause form (technical)
- Something: examples - How to use Skolem functions to say "some"
- Out of Sorts (page 1) - How to do without multiple sorts. Page 1 of 2.
- Out of Sorts (Page 2) - How to do without multiple sorts. Page 2 of 2.
Nuts And Bolts
- Buttons - The LOAD, SAVE, TEXT and CLEAR buttons.
- Settings - Effects achievable using the SETTINGS button
- Using the Diagnoser - Help when no solution is found
- Error Messages - Making sense of what the solver says when it complains (long page).
- Cryptic Error Messages - Obscure messages returned by the parser, with explanations.
- Syntax - Formal definition of the input language (technical)