Type Members

1.  case class AToken(rule: String, name: Option[LambdaAST], antecedent: List[LambdaAST], succedent: List[LambdaAST]) extends Token with Product with Serializable

   An AToken represents an Axiom declaration or Definition declaration.

   An AToken represents an Axiom declaration or Definition declaration.

   rule

   either "AXIOMDEF", "PREDDEF" or"FUNDEF"

   name

   the (unique) name of the definition/axiom

   antecedent

   the antecedent of the declaration sequent (not yet typechecked)

   succedent

   the succedent of the declaration sequent (not yet typechecked)

2.  class DeclarationParser extends LLKASTParser
3.  case class ExtendedProofDatabase(eproofs: Map[Formula, LKProof], eaxioms: Map[Formula, Formula], edefinitions: Map[Const, Expr]) extends Product with Serializable

   An extended proof database allows to label subproofs by formulas.

   An extended proof database allows to label subproofs by formulas. It provides mappings from formulas to proofs additionally to the list of pairs.

4.  class HybridLatexParserException extends Exception
5.  class LLKASTParser extends JavaTokenParsers with PackratParsers
6.  class LLKExporter extends AnyRef
7.  class LLKFormulaParser extends AnyRef
8.  class LLKProofParser extends DeclarationParser with LatexReplacementParser with TokenToLKConverter
9.  trait LatexReplacementParser extends DeclarationParser

   This code works around some limitations of latex syntax and adds alternative syntax for abstraction, application and adds support of some macros used in the n-tape proof.

10.  case class RToken(rule: String, name: Option[LambdaAST], antecedent: List[LambdaAST], succedent: List[LambdaAST], sub: List[(Var, LambdaAST)]) extends Token with Product with Serializable

    A RToken represents a rule application.

    A RToken represents a rule application.

    rule

    One out of "AX", "ALLL", "ALLR", "EXL", "EXR", "ANDL", "ANDR", "ORL", "ORR", "IMPL", "IMPR", "NEGL", "NEGR", "CUT", "EQL", "EQR", "WEAKL", "WEAKR", "CONTRL", "CONTRR", "DEF", "BETA", "INSTAXIOM"

    name

    quantifier rules allow optional specification of the subsitution term, definitions and axiom instantiations take the referenced declaration, etc.

    antecedent

    the antecedent of the declaration sequent (not yet typechecked)

    succedent

    the antecedent of the declaration sequent (not yet typechecked)

    sub

    some rules like axiom instantiation specify substitutions, which are passed as list of var-term pairs

11.  case class TToken(decltype: String, names: List[String], types: Ty) extends Token with Product with Serializable

    A TToken represents an LLK type declaration.

    A TToken represents an LLK type declaration.

    decltype

    either "VARDEC" or "CONSTDEC"

    names

    a list of symbol names

    types

    the assigned type

12.  abstract class Token extends AnyRef

    The abstract class for tokens of an llk proof.

    The abstract class for tokens of an llk proof. TTokens represent type declarations, ATokens represent axiom and definition declarations, and RTokens represent a rule inference.

13.  trait TokenToLKConverter extends AnyRef

    This implements the second parsing pass, converting hlk Tokens to an LK Proof.

    This implements the second parsing pass, converting hlk Tokens to an LK Proof. HybridLatexParser inherits from TokenToLKConverter to have a common interface, but the code here is only dependent on the AST. It uses the ASTtoHOL object to create Exprs from hol ASTs.