Type Members

1.  sealed abstract class BinaryConnective extends Connective
2.  final case class BinaryFormula(connective: BinaryConnective, left: Formula, right: Formula) extends Formula with Product with Serializable
3.  final case class ConditionalTerm(condition: Formula, thn: Formula, els: Formula) extends Formula with Product with Serializable
4.  sealed abstract class Connective extends AnyRef
5.  final case class ConnectiveTerm(conn: Connective) extends Formula with Product with Serializable

   Connective as proper term.

6.  sealed abstract class DefinedTH1Constant extends AnyRef

   Special kind of interpreted TPTP constants that do not start with a dollar sign.

   Special kind of interpreted TPTP constants that do not start with a dollar sign. Used in TH1 for polymorphic constant symbols that correspond to quantification, equality, etc.

7.  final case class DefinedTH1ConstantTerm(constant: DefinedTH1Constant) extends Formula with Product with Serializable
8.  final case class DistinctObject(name: String) extends Formula with Product with Serializable

   An object that is unequal to every DistinctObject with a different name.

9.  sealed abstract class Formula extends AnyRef
10.  final case class FunctionTerm(f: String, args: Seq[Formula]) extends Formula with Product with Serializable

    Constant symbols c or FOF-style functional expressions f(c).

    Constant symbols c or FOF-style functional expressions f(c). 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

11.  final case class LetTerm(typing: Map[String, Type], binding: Seq[(Formula, Formula)], body: Formula) extends Formula with Product with Serializable
12.  final case class Logical(formula: Formula) extends Statement with Product with Serializable
13.  final case class NonclassicalBox(index: Option[Formula]) extends VararyNonclassicalOperator with Product with Serializable
14.  final case class NonclassicalCone(index: Option[Formula]) extends VararyNonclassicalOperator with Product with Serializable
15.  final case class NonclassicalDiamond(index: Option[Formula]) extends VararyNonclassicalOperator with Product with Serializable
16.  final case class NonclassicalLongOperator(name: String, index: Option[Formula], parameters: Seq[(Formula, Formula)]) extends VararyNonclassicalOperator with Product with Serializable
17.  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. When used with short connectives ([.], <.>, /.\) it will print as unary connective (without @ sign).

18.  final case class NumberTerm(value: Number) extends Formula with Product with Serializable
19.  final case class QuantifiedFormula(quantifier: Quantifier, variableList: Seq[TypedVariable], body: Formula) extends Formula with Product with Serializable
20.  sealed abstract class Quantifier extends AnyRef
21.  final case class Sequent(lhs: Seq[Formula], rhs: Seq[Formula]) extends Statement with Product with Serializable
22.  sealed abstract class Statement extends AnyRef
23.  final case class Tuple(elements: Seq[Formula]) extends Formula with Product with Serializable
24.  type Type = Formula
25.  type TypedVariable = (String, Type)
26.  final case class Typing(atom: String, typ: Type) extends Statement with Product with Serializable
27.  sealed abstract class UnaryConnective extends Connective
28.  final case class UnaryFormula(connective: UnaryConnective, body: Formula) extends Formula with Product with Serializable
29.  sealed abstract class VararyNonclassicalOperator extends AnyRef
30.  final case class Variable(name: String) extends Formula with Product with Serializable

    A TPTP variable.

    A TPTP variable. Precondition for creating a Variable object: name is uppercase.