Non-classical Logics
by
Tobias Gleißner,
Alexander Steen,
Geoff Sutcliffe,
Christoph Benzmüller
Motivation
Extension of the TPTP TFX and THF dialects to support a wide range of
non-classical logics with
- Minimal syntactic changes
- User-friendly syntax (easy reading and writing of problems)
- Developer-friendly syntax (easy parsing, minimal cases to consider e.g.,
when defining semantics)
- Uniform syntax for all non-classical logics
- Consistency throughout TPTP dialects
Overview
- A long form for all connectives of any non-classical logic.
The long form contains the full name of a connective as defined words
e.g. $permissible.
- A short form for selected connectives in selected non-classical logics,
e.g., [.] and <.> for $necessary and
$possible in alethic modal logic.
- A seperate specification of the semantics.
The descriptions and examples below are in terms of alethic modal logic.
The syntax offers much more - see the section on the
exotic future below.
Connectives Long Form
Connectives belonging to a logic get unique defined names, e.g.,
$necessary.
The connective is written in {} brackets, and the application is
functional.
The BNF grammar is
here.
Examples:
tff(pigs_might_fly_type,type,pigs_might_fly: $o ).
tff(no_flying_pigs,axiom,
~ {$possible}(pigs_might_fly) ).
tff(something_is_possible,axiom,
? [P: $o] : {$possible}(P) ).
thf(forbidden_flying_pigs,axiom,
{$forbidden} @ pigs_might_fly ).
thf(everything_is_permissible,axiom,
! [P: $o] : ( {$permissible} @ P ) ).
Connectives may have a list of parameters, where a parameter is one of:
- A optional single initial index term starting with #.
The index can be any constant (uninterpreted constant, number, TPTP
defined constant) of any type.
The TPTP might provide predefined values, e.g., $past, for
individual logics.
Indices are distinct from each other and from object logic terms.
Examples:
tff(an_individual_type,type,me: $i ).
tff(for_me_it_is_possible,axiom,
{$possible(#me)}(pigs_might_fly) ).
tff(for_me_something_is_possible,axiom,
? [P: $o] : {$possible(#me)}(P) ).
thf(agent_type,type,agent: $tType ).
thf(archer_type,type,archer: agent ).
thf(archer_knows_flying_pigs,axiom,
{$knows(#archer)} @ pigs_might_fly ).
thf(for_archer_everything_is_permissible,axiom,
! [P: $o] : ( {$permissible(#archer)} @ P ) ).
- A key-value expression of form LHS := RHS
where LHS is a TPTP defined constant, and RHS is a term
(for TFF a tff_atomic_formula, for THF a
thf_fof_function).
This is not used in alethic modal logics, but in other logics, e.g.,
epistemic logic ...
{$knows(#1)}({$common($group:=[2,3,4])}(something_commonly_known_by_agents_2_3_and_4))
Connectives Short Form
The short forms provide shorthand for the long forms.
Two short forms are available in alethic modal logics:
[...], <...>.
The short forms are associated by TPTP standards with specific long forms in
specific logics, e.g., in alethic modal logic [...] is short for
{$necessary:...} and <...> is short for
{$possible:...}.
There might not be a short form for every long form in a given logic.
The short forms may be parameterized by an index, but nothing more.
A non-indexed short form has a period in the brackets.
The BNF grammar is
here.
Examples:
tff(no_flying_pigs,axiom,
~ <.>(pigs_might_fly) ).
tff(for_me_it_is_possible,axiom,
<#me>(pigs_might_fly) ).
thf(forbidden_flying_pigs,axiom,
<.> @ pigs_might_fly ).
thf(archer_knows_flying_pigs,axiom,
[#archer] @ pigs_might_fly ).
Short forms and long forms can be used together, e.g., itâ€™s OK to use
{$necessary} and [.] in the same problem or formula.
Semantics Specification
Annotated formulae with the (new) role logic are used to specify
the semantics of the logic.
Such a formula begins with the keyword for the logic, e.g.,
$modal, $alethic_modal, $deontic_modal,
$epistemic_modal, followed by == and a list of properties
value assignments.
Each specification is the property name, followed by == and either
a value or a tuple of specification details.
If the first element of a list of details is a value, that is the default
value for all cases that are not specified in the rest of the list.
Each detail after the optional default value is the name of a relevant part
of the vocabulary of the problem, followed by == and a value
for that named part.
The BNF grammar is
here.
The semantic specification typically comes first in a problem file.
A logic specification changes the meaning of things such as the boolean
type $o, universal quantification with !, etc.
Their existing meaning in classical logic should not be confused with the
meaning in the declared logic.
For alethic modal logics the properties that may be specified are
$constants, $quantification, $consequence, and
$modalities.
The $constants, $quantification, and $modalities
may have individual values for constants and types, and the
$consequence may have individual values for named axioms.
- $constants
- $rigid - Rigid constants are independent of worlds.
- $flexible - Flexible constants are dependent on worlds.
- $quantification
- $constant - Constant domain semantics has all world's
domains fixed the same.
- $varying - Varying domain semantics has (potentially)
different domains for each world.
- $cumulative - Cumulative domain semantics and varying,
and the domain of each world is a superset of the domains of the
worlds from which it can be reached.
- $decreasing - Decreasing domain semantics and varying,
and the domain of each world is a subset of the domains of the
worlds from which it can be reached.
- $consequence
- $local - The formula is assumed to be true in the current
world.
- $global - The formula is assumed to be true in all worlds.
- $modalities - These are specified in this
Wikipedia page.
See
CorrectSpecifications.p for examples.
The grammar is not very restrictive on purpose, to enable working with other
logics as well.
It is possible to create a lot of nonsense specifications, and to say the
same thing in different meaningful ways.
A tool to check the sanity of a specification is available.
Examples
These examples can be run in Leo-III within
SystemOnTPTP.
Leo-III embeds non-classical logic problems into plain THF, and solves the
THF problem.
The embedding tool is available as Logic2THF in
SystemB4TPTP, the
output from which can be given to any THF system.
- Wise men puzzle, TFF, epistemic modal
logic, long connectives, indices and constants overlap
- Wise men puzzle, TFF, epistemic modal
logic, long connectives, indices and constants distinct
- Wise men puzzle, TFF, generic modal
logic, short connectives, indices and constants distinct
- Wise men puzzle, THF, epistemic modal
logic, long connectives, indices and constants overlap
- Wise men puzzle, THF, epistemic modal
logic, long connectives, indices and constants distinct
- Wise men puzzle, THF, generic modal
logic, short connectives, indices and constants distinct
- Bungling chemists, TFF, alethic modal
logic, short connectives
- Bungling chemists, THF, alethic modal
logic, long connectives
- Barcan formula, TFF, generic modal
logic, short connectives
- Converse Barcan formula, TFF, generic
modal logic, short connectives
Logic Documentation
The various logics, the syntax used, the axiom schemes, and the semantics
specification, are being semi-formally documented in a machine readable form.
This work is available in the
Logics directory of the Github repository.
Exotic Future
The use of the TPTP framework for non-classical logics, as presented so far,
is conservative, adopting only widely accepted structures in alethic modal
logics.
The TPTP framework is capable of much more.
Some of our ideas are listed here, some relevant and unpolished files are
in the
ExoticFuture directory, and feedback is welcome.
- Using object logic terms, including variables, as indices.
- Non-alethic modal logics are already supported in the syntax, and tool
support will be added.
- Encoding of description logic (ALC, ALCQI) problems in TPTP description
logic format (an old TPTP effort) into modal logic.
- Two more short forms {...}, and (...).
- In logic specifications that $modalities may be written as
THF formulae, or as frame conditions using $r as the
accessibility relation.
- Problems with multiple logics together.
(Short forms may not be used when multiple logics are used together - the
long forms have to be used, to avoid conflicting uses of the short forms.)
- Problems with semantics templates that represent multiple semantics
specifications, and a tool to burst these out into individual problem
files.
- More (non-modal) logics.
- More and more