// A vocabulary defines types and signatures of functions and predicates.
vocabulary MyVocabulary {
// For classical first-order logic, a single type T is sufficient.
type T
// All predicates must be listed here:
R(T,T) // R is a predicate of arity 2
S(T) // S is a predicate of arity 1
// All functions must be listed here:
f(T) : T // f is a function of arity 1
c : T // c is a function of arity 0
d : T // d is a function of arity 0
}
// A theory consists of a set of well formed formulas.
// Each formula is terminated by full stop.
// Symbols are pretty-printed:
// - conjunction: &
// - disjunction: |
// - implication: =>
// - equivalence: <=>
// - negation: ~
// - for all: !
// - exists: ?
// Quantifiers are followed by a space-separated list of variables. After that, there is a semicolon and the subformula on which the quantifiers are applied.
theory MyTheory : MyVocabulary {
!x y z: R(x,y) | R(z,c) | S(z).
!u v w: ~R(f(u),u) | ~R(v,w).
~S(f(d)).
}
// Here we define a partial structure. For our purposes, we only specify the domain of T.
structure MyStructure : MyVocabulary {
T = {0..1}
}
// This is the entry point. For our purposes, we can leave it as it is.
procedure main() {
printmodels(modelexpand(MyTheory, MyStructure))
}