FO(.)

FO(.) (aka FO-dot) is a Knowledge representation language based on First-order logic. It has 4 types of statements:

Function and predicate declarations,
Axiom, i.e., logic sentences about possible worlds,
Definitions that specify a unique interpretation of a defined symbol, given the interpretation of its parameters. Definitions can be inductive.
Enumerations, i.e., definitions of symbols by enumeration.

An FO-dot knowledge base cannot be run. It is a "bag of information", to be used as input to various generic reasoning algorithms: e.g., determine relevant questions, compute consequences of new facts, and explain them.

FO-dot is used by these reasoning engines:

www.idp-z3.be

IDP

FOLASP

Example

Let's represent the following voting laws in FO(.):

you must be 18 year old to vote;
if the law is prescriptive, voting is mandatory.

vocabulary V{
  age18, vote, prescriptive: () -> Bool // predicate declaration
}
theory T:V {
  ~age18() => ~vote().  // axiom: if you are not 18, you may not vote.
  prescriptive() => (age18() => vote()).  // axiom, if prescriptive: if you are 18, you must vote
}

Such knowledge base can be turned automatically into an Interactive Lawyer (see here).

Reference

The FO(.) language