Type Members

1.  final case class Assignment(lhs: AtomicTerm, rhs: Term) extends Formula with Product with Serializable
2.  final case class AtomicFormula(f: String, args: Seq[Term]) extends Formula with Product with Serializable

   Important: f may be a dollar word, a dollar dollar word (plain string starting with $ or $$), a lower word (plain string with certain restrictions) or a single quoted TPTP atomic word.

   Important: f may be a dollar word, a dollar dollar word (plain string starting with $ or $$), a lower word (plain string with certain restrictions) or a single quoted TPTP atomic word. In the latter case, non-lower word atomic words are enclosed in single quotes, e.g. '...'. Any string that is neither a dollar/dollardollar word, a lower word, or a single quoted, is an invalid value for f. Use

   TPTP.isLowerWord

   to check if the string a valid (non-quoted) value for f, or transform via

   TPTP.convertStringToAtomicWord

   if necessary before. Quotes and Backslashes are not escaped in the representation, but will (need to) be escaped for pretty printing.

   See also

   TPTP.convertStringToAtomicWord

3.  final case class AtomicTerm(f: String, args: Seq[Term]) extends Term with Product with Serializable

   A term expression that is either (1) a constant symbol c, or (2) a function expression f(arg1,arg2,...,argN).

   A term expression that is either (1) a constant symbol c, or (2) a function expression f(arg1,arg2,...,argN). In case (1) it holds that args.isEmpty; in case (2) it holds that args.nonEmpty.

   f may be a dollar word, a dollar dollar word (plain string starting with $ or $$), a lower word (plain string with certain restrictions) or a single quoted TPTP atomic word. In the latter case, non-lower word atomic words are enclosed in single quotes, e.g. '...'. Any string that is neither a dollar/dollardollar word, a lower word, or a single quoted, is an invalid value for f. Use

   TPTP.isLowerWord

   to check if the string a valid (non-quoted) value for f, or transform via

   TPTP.convertStringToAtomicWord

   if necessary before.

   f

   The name of the constant or function symbol

   args

   The arguments arg1, arg2, ... of the function expression as sequence of Terms. The empty sequence if the term is a constant symbol.

   See also

   TPTP.convertStringToAtomicWord

4.  final case class AtomicType(name: String, args: Seq[Type]) extends Type with Product with Serializable
5.  sealed abstract class BinaryConnective extends Connective
6.  final case class BinaryFormula(connective: BinaryConnective, left: Formula, right: Formula) extends Formula with Product with Serializable
7.  final case class ConditionalFormula(condition: Formula, thn: Term, els: Term) extends Formula with Product with Serializable
8.  sealed abstract class Connective extends AnyRef

   Logical connectives in TFF, includes UnaryConnectives and BinaryConnectives.

9.  final case class DistinctObject(name: String) extends Term with Product with Serializable

   A term that represents an object that stands for itself, i.e., a distinct object with name N is interpreted to be unequal to every other distinct object with name N' iff N != N'.

   A term that represents an object that stands for itself, i.e., a distinct object with name N is interpreted to be unequal to every other distinct object with name N' iff N != N'.

   name

   The name of the distinct object. Must start and end with a double quote, i.e., name = "<somename>".

   Note

   Names of distinct objects are double quoted; and the double quotes are considered part of its name. That means that the DistinctObject "something" is different from the AtomicTerm something, but may, of course, be equal to it.

10.  final case class Equality(left: Term, right: Term) extends Formula with Product with Serializable
11.  sealed abstract class Formula extends AnyRef
12.  final case class FormulaTerm(formula: Formula) extends Term with Product with Serializable

    A formula in term position as used in TFX (FOOL logic).

    A formula in term position as used in TFX (FOOL logic). Terms of this kind can safely be ignored if TFX is not planned to be supported; and they will never be created by the leo.modules.input.TPTPParser for inputs that are non-TFX TFF formulas inputs.

    formula

    The Formula in term position.

    Note

    The leo.modules.input.TPTPParser will never yield expressions containing FormulaTerms that themself wrap single (formula) variables or atomic formulas, i.e., the expressions

    FormulaTerm(FormulaVariable(x))

    and

    FormulaTerm(AtomicFormula(f, args))

    are never created. Instead, an equivalent term expressions

    Variable(x)

    and

    AtomicTerm(f, args)

    , respectively, are created. This means that also for Boolean-typed variables or predicate applications, a representation as Term is returned. Of course, users may create such instances and handle them appropriately in their application.

13.  final case class FormulaVariable(name: String) extends Formula with Product with Serializable
14.  final case class Inequality(left: Term, right: Term) extends Formula with Product with Serializable
15.  final case class LetFormula(typing: Map[String, Type], binding: Seq[(Term, Term)], body: Term) extends Formula with Product with Serializable
16.  final case class Logical(formula: Formula) extends Statement with Product with Serializable
17.  final case class MappingType(left: Seq[Type], right: Type) extends Type with Product with Serializable
18.  final case class MetaIdentity(lhs: AtomicTerm, rhs: Term) extends Formula with Product with Serializable
19.  final case class NonclassicalBox(index: Option[Term]) extends VararyNonclassicalOperator with Product with Serializable
20.  final case class NonclassicalCone(index: Option[Term]) extends VararyNonclassicalOperator with Product with Serializable
21.  final case class NonclassicalDiamond(index: Option[Term]) extends VararyNonclassicalOperator with Product with Serializable
22.  final case class NonclassicalLongOperator(name: String, index: Option[Term], parameters: Seq[(Term, Term)]) extends VararyNonclassicalOperator with Product with Serializable
23.  final case class NonclassicalPolyaryFormula(connective: VararyNonclassicalOperator, args: Seq[Formula]) extends Formula with Product with Serializable

    Non-classical formula as per recent TPTP NHF standard.

    Non-classical formula as per recent TPTP NHF standard. The connective is n-ary with arbitrary n, see the TPTP documentation which connective names have pre-defined meaning.

24.  final case class NumberTerm(value: Number) extends Term with Product with Serializable

    A term that represents a number.

    A term that represents a number. The numbers are given by a Number object.

    value

    The Number as a TFF term.

25.  final case class QuantifiedFormula(quantifier: Quantifier, variableList: Seq[TypedVariable], body: Formula) extends Formula with Product with Serializable
26.  final case class QuantifiedType(variables: Seq[TypedVariable], body: Type) extends Type with Product with Serializable
27.  sealed abstract class Quantifier extends AnyRef
28.  final case class Sequent(lhs: Seq[Term], rhs: Seq[Term]) extends Statement with Product with Serializable
29.  sealed abstract class Statement extends AnyRef
30.  sealed abstract class Term extends AnyRef

    Syntactical terms of the TFF language, i.e, first-order terms being one of:

    Syntactical terms of the TFF language, i.e, first-order terms being one of:

    • AtomicTerm
    • Variable
    • DistinctObject
    • NumberTerm
    • FormulaTerm*
    • Tuple*

    Elements marked with * are part of the extended TFF format (TFX) and may safely be ignored if TFX is not to be supported. They will never be created by the leo.modules.input.TPTPParser for non-TFX TFF inputs. In match-case statements, non-exhaustiveness warnings may be suppressed using the scala.unchecked annotation.

31.  final case class Tuple(elements: Seq[Term]) extends Term with Product with Serializable

    A tuple as TFF term.

    A tuple as TFF term. Terms of this kind can safely be ignored if TFX is not planned to be supported; and they will never be created by the leo.modules.input.TPTPParser for inputs that are non-TFX TFF formulas inputs.

    elements

    The entries of the tuple.

32.  final case class TupleType(components: Seq[Type]) extends Type with Product with Serializable
33.  sealed abstract class Type extends AnyRef
34.  final case class TypeVariable(name: String) extends Type with Product with Serializable
35.  type TypedVariable = (String, Option[Type])
36.  final case class Typing(atom: String, typ: Type) extends Statement with Product with Serializable
37.  sealed abstract class UnaryConnective extends Connective
38.  final case class UnaryFormula(connective: UnaryConnective, body: Formula) extends Formula with Product with Serializable
39.  sealed abstract class VararyNonclassicalOperator extends AnyRef
40.  final case class Variable(name: String) extends Term with Product with Serializable

    A term that represents an uppercase variable that is bound by some quantifier.

    A term that represents an uppercase variable that is bound by some quantifier.

    name

    The name of the variable (needs to be uppercase).

    Note

    In the context of TFX, this may also be a Boolean-typed variable (i.e., representing a formula). If TFX is not to be supported, it can be assumed that this only represents proper term variables.

    ,

    In the context of TF1, this may also be a type variable (i.e., representing a type). If TF1 is not to be supported, it can be assumed that this only represents proper term variables.