About

Toss is a program which allows to explore the use of logic and terms in various models. On the static side, you can draw graphs and check their properties, axioms and reductions. Then, on the dynamic side, you can model multi-player games with both discrete and continuous dynamics. You can play the games, generate strategies automatically and analyse possible behaviours with respect to various logic formulas. For example, did you ever wonder how your favorite game would feel if you removed the middle of the board? With Toss, it is easy to experiment!

Play Online Against Toss

More Games

News

• 08/02/14   Documentation and bugfixes so that everything compiles on Linux and OSX.
• 24/11/13   Correcting a bug in server response parameters makes TossServer far more reliable
• 10/11/13   Toss release 1.0 similar to 0.9 but with corrected bugs and improved speed
• 05/10/13   Improvements in mpisat and mpiqbf interfaces to lingeling and depqbf
• 17/09/13   Lingeling binding to use it in mpisat
• 27/08/13   Mpiqbf — an MPI-based distributed QBF solver that uses a depqbf binding.
• 23/08/13   Mpisat — first commit of our MPI-based distributed sat-solver
• 14/08/13   Using order encoding for arithmetic operations, better convnets learning
• 24/07/13   First tests of sat-solver based learning of convolutional neural networks
• 14/07/13   Generate propositional encodings for arithmetic operations
• 04/07/13   Support for external sat-solvers including lingeling
• 08/06/13   Generate QBF formulas for winning in X moves in Toss games
• 24/05/13   Speed improvements and first automatic translation of amazons from GDL
• 12/05/13   Test driver executable allows to compare Toss speed with other GGP engines
• 14/04/13   Hash-consing for Boolean formulas in the new QBF module
• 26/03/13   Toss release 0.9 with many new features and corrected bugs
• 20/03/13   Game learning now works faster using sat-solver based learning
• 02/03/13   Bindings to MiniSat and GlueMiniSat for native-code version
• 23/02/13   Program synthesis work: we can find Lfp formulas given second-order specification
• 17/02/16   Symbolic evaluation enabled for fixed-points, extending the reach of Toss symbolic system considerably
• 09/02/13   Multiple bugs corrected in Toss web Client and other modules
• 04/02/13   Performance improvements in handling propositional formulas
• 29/01/13   New Toss Client version live on tPlay
• 27/01/13   Variable board sizes supported in Toss Client
• 25/01/13   Taking back moves in Toss Client
• 20/01/13   Hash-consed formulas support added and used to speed up main solver cache
• 08/12/12   Support for constants in formulas, structures, solver, and reductions
• 29/11/12   Bash interface to reduction finding functions
• 19/11/12   First JS interface to Reduction Finder
• 10/11/12   Debugging and extending reduction finder
• 08/11/12   First interface to our Vision Explorer (Chrome only for now)
• 04/11/12   Two variants of the Canny edge detection algorithm in Toss
• 29/10/12   Starting OCaml vision algorithms work, matrix syntax extension
• 24/10/12   First interface to the Terms and Types Explorer
• 28/09/12   Separating relational structure explorer and reduction finder
• 20/09/12   Replacing rewriting with isa-match further unifies terms and types
• 17/09/12   Removing MSO from formulas, only full SO syntax remains
• 12/09/12   Extending and improving the new type system and library
• 05/09/12   New term parsing and rewriting library based on new type system
• 31/08/12   Optional upper bounds for type variables, parsing preferences now encoded in type system
• 30/08/12   Basic SAT-solver implemented using Diagrams and hash-consing
• 21/08/12   Replacing MGU with GLB+LUB gives more general term unification
• 11/08/12   HashCons module for hash-consed types tested on Diagrams
• 09/08/12   Merging terms and types internally opens new possibilities
• 30/07/12   Allowing imperative rule syntax, porting Tic-Tac-Toe
• 21/07/12   Extended relational structure explorer, reduction finding stubs
• 15/07/12   New representation in Term and ISA-matching
• 04/07/12   First version of the Relational Structures Explorer with SO finding
• 27/06/12   Second-order (SO) evaluation by reduction to QBF
• 25/06/12   Full support for Unicode in formulas
• 07/06/12   Switching to a new ODE solver which uses the Cash-Karp method
• 02/06/12   Starting work on an interface for structures and formula evaluation
• 27/05/12   First structures defined using the term rewriting system syntax
• 24/05/12   Code for Term functions cleaned up and made JS compatible
• 13/05/12   Toss release 0.8 with full JS compatibility with dynamics
• 04/05/12   Dynamics debugged and animations now work in the JS interface
• 04/05/12   Old rewriting example works with the JS interface
• 25/04/12   Work on positioning with the JS interface
• 30/03/12   Adding Hnefatafl to example Toss games
• 21/03/12   Toss Client and website updated to a cleaned-up JS version
• 09/03/12   First completely working all-JS Toss version
• 05/03/12   Fully integrated OCaml and JS debugging and logs
• 27/02/12   Compiled resources to access files from JS
• 18/02/12   Integrating OCaml and JS unit tests
• 11/02/12   Starting systematic unit tests of JS interface
• 06/02/12   Toss release 0.7 with many improvements
• 04/02/12   Definitions use play history: new Chess toss file
• 02/02/12   Improved stand-alone JS interface with menhirLib
• 31/01/12   First stand-alone JS interface (with js_of_ocaml)
• 22/01/12   Learning Connect4 and Gomoku from videos
• 21/01/12   Learning Breakthrough and Pawn-Whopping videos
• 17/01/12   Integrating game learning logic and video stuff
• 06/01/12   Parametrized grid detection for video
• 28/12/11   Game video recognition improved with Hough lines
• 10/12/11   Starting work on game recognition from video
• 24/10/11   Learning games from examples in web interface
• 19/10/11   Games learning engine and first buttons in the UI
• 14/09/11   Simple editing of games added to web interface
• 31/07/11   Store date and time of moves in games
• 30/07/11   Corrected opponent lists in the Profile tab
• 03/07/11   Added game descriptions viewable when playing
• 30/06/11   View previous moves in a play
• 27/06/11   Tabs and searching opponents in the profile page
• 22/06/11   Better organized lists of plays
• 19/06/11   News section on the front page of tPlay
• 15/06/11   Bug with underscores in user names corrected
• 10/06/11   New register site handles forgotten passwords
• 05/06/11   Pre-caching client states improves response times
• 03/06/11   Corrected tPlay 1.1 app accepted on App Store
• 30/05/11   Large restructuring of JavaScript code finished
• 24/05/11   Breakthrough generation from examples in SVN
• 23/05/11   First tPlay application accepted on App Store

More

Create New Games

First explore relational structures and then go to the create games page to learn how to build new games with Toss.

Toss Features

Games in Toss are defined as mathematical structures and moves by structure rewriting rules. Payoffs are given by formulas of monadic second-order logic with real values.

• Structures can have an arbitrary number of relations of any arity and additional real-valued functions (explore).
• Rules work by matching arbitrary left-hand side structures and replacing them with the right-hand side structure.
• Logic is used for rule constraints and payoffs. We support full monadic second-order logic with additional real arithmetic.
• Solver in Toss is optimized: it does quantifier elimination and formula decomposition (test).
• Continuous dynamics can be specified using ODEs. This allows for example to simulate movements and collisions.