apollo-backend/eu.yeger.apollo.shared.model.fol

Package-level declarations

Types

Represents an FOL variable bound by a Quantifier.

sealed class Constant : Formula

Represents an FOL constant that is either True or False.

sealed class FOLEntity

Provides helper methods for String representations of FOL entities (formulas and terms).

Represents an FOL formula and contains methods for ModelChecking.

data class FormulaHead(val formula: Formula, val symbolTable: Map<String, String>)

This class is used to store metadata for a FOLFormula.

sealed class Function : Term

Represents a Term function.

data class ModelCheckerTrace(val formula: String, val description: TranslationDTO, val isModel: Boolean, val shouldBeModel: Boolean, val children: List<ModelCheckerTrace>? = null)

Trace of the ModelChecking algorithm. Contains information about a single check and its child checks.

sealed class Operator : Formula

Represents an FOL operator.

Represents an FOL quantifier.

sealed class Relation : Formula

Represents an FOL relation.

data class SymbolTable(val unarySymbols: Map<String, Set<Node>>, val binarySymbols: Map<String, Set<Edge>>, val symbolTypes: Map<String, String>)

DTO containing precalculated meta information for the ModelChecking algorithm.

sealed class Term : FOLEntity

Represents an FOL term (BoundVariable or Function).