zoxiy user guide

--- by s.butterfill@warwick.ac.uk

Some notes on using zoxiy to complete logic exercises (writing proofs, creating counterexamples, ...).

Start here:


There are logic exercises associated with each lecture. This is how to complete them ...

For students:

Symbols and Words

proof ex-proof ex-trans

When you use zoxiy you can type words instead of using symbols. But which words stand for which symbols? Here’s a list.


definitions ex-create

Introduces the notion of identity used in studying first-order logic. Includes example argument and the two principles. Also demonstrates how to assign names in zoxiy, and using zoxiy to make identity statements true and false.

Contradictions, Logical Truths and Logical Possibilities

definitions ex-tt

Illustrates and defines the terms ‘contradiction’, ‘logical truth’ and ‘logical possibility’. Describes how to recognise these from truth tables. Demonstrates using zoxiy to construct truth-tables and answer questions about contradictions, logical truths and logical possibilities.

Quantifer Rules: ∃Elim with zoxiy

proof ex-proof

Explains how to do proofs involving quantifier rules with zoxiy. (Where you need to put the name ‘a’ in a box, write ‘[a]’.)

zoxiy: Creating Possible Situations


Describes how to create possible situations in logic-ex.

Formal Counterexamples with zoxiy

counterexamples ex-counter


definitions ex-create

Explains the notion of a counterexample. Discusses a counterexample to a simple argument. Demonstrates using zoxiy to construct a counterexample involving shape and size properties.

Formal Proof: ∧Elim and ∧Intro

proof ex-proof

Introduces and illustrates the use of rules of proof for conjunction. Explains how to create proofs using logic-ex.

Subproofs with zoxiy

proof proof-example ex-proof

Introduction to the rules of proof for →, →Intro and →Elim. This is the first time subproofs are used. Also illustrates a proof without any premises. The proof is from premises P→Q and Q→R to conclusion P→R.

Zoxiy world predicates


Defines the predicates such as ‘Happy(x)’ and ‘Crying(x)’ used in creating possible worlds.

Creating possible situations


A quick guide to creating possible situations in zoxiy.

For tutors:

Monitoring Students’ Progress


How to check what students’ have completed, whether they are getting the answers right and what their answers are.

Creating Your Own Exercises


In zoxiy, an exercise is a url. You can set exercises just by creating a list of urls.