Packages

object Logic

Linear Supertypes
AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. Logic
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Type Members

  1. final case class Atoms (inHead: Set[Atom], inFormula: Set[Atom]) extends Product with Serializable

    Represents the set of atoms in the heads of clauses and in the bodies (formulas) of clauses.

  2. final class CyclicNegation extends LogicException
  3. final class InitialContradictions extends LogicException
  4. final class InitialOverlap extends LogicException
  5. sealed abstract class LogicException extends AnyRef
  6. final class Matched extends AnyRef

    Tracks proven atoms in the reverse order they were proved.

Value Members

  1. final def !=(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  2. final def ##(): Int
    Definition Classes
    AnyRef → Any
  3. final def ==(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  4. def applyAll(c: Clause, facts: Set[Literal]): Option[Clause]
  5. def applyAll(cs: Clauses, facts: Set[Literal]): Option[Clauses]

    Applies known facts to clauses, deriving a new, possibly empty list of clauses.

    Applies known facts to clauses, deriving a new, possibly empty list of clauses. 1. If a fact is in the body of a clause, the derived clause has that fact removed from the body. 2. If the negation of a fact is in a body of a clause, that clause fails and is removed. 3. If a fact or its negation is in the head of a clause, the derived clause has that fact (or its negation) removed from the head. 4. If a head is empty, the clause proves nothing and is removed.

    NOTE: empty bodies do not cause a clause to succeed yet. All known facts must be applied before this can be done in order to avoid inconsistencies. Precondition: no contradictions in facts Postcondition: no atom in facts is present in the result Postcondition: No clauses have an empty head

  6. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  7. def atoms(formula: Formula): Set[Atom]

    Computes the set of all atoms in formula.

  8. def atoms(cs: Clauses): Atoms

    Computes the atoms in the heads and bodies of the clauses in clause.

  9. def clone(): AnyRef
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  10. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  11. def equals(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  12. def finalize(): Unit
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  13. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
  14. def hasNegatedDependency(clauses: Seq[Clause], posDeps: Relation[Atom, Atom], negDeps: Relation[Atom, Atom]): List[Atom]

    Computes the set of atoms in clauses that directly or transitively take a negated atom as input.

    Computes the set of atoms in clauses that directly or transitively take a negated atom as input. For example, for the following clauses, this method would return List(a, d) : a :- b, not c d :- a

    Annotations
    @tailrec()
  15. def hashCode(): Int
    Definition Classes
    AnyRef → Any
  16. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  17. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  18. final def notify(): Unit
    Definition Classes
    AnyRef
  19. final def notifyAll(): Unit
    Definition Classes
    AnyRef
  20. def reduce(clauses: Clauses, initialFacts: Set[Literal]): Either[LogicException, Matched]

    Computes the variables in the unique stable model for the program represented by clauses and initialFacts.

    Computes the variables in the unique stable model for the program represented by clauses and initialFacts. clause may not have any negative feedback (that is, negation is acyclic) and initialFacts cannot be in the head of any clauses in clause. These restrictions ensure that the logic program has a unique minimal model.

  21. def reduceAll(clauses: List[Clause], initialFacts: Set[Literal]): Either[LogicException, Matched]
  22. def substitute(formula: Formula, facts: Set[Literal]): Option[Formula]

    Derives the formula that results from substituting facts into formula.

    Derives the formula that results from substituting facts into formula.

    Annotations
    @tailrec()
  23. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  24. def toString(): String
    Definition Classes
    AnyRef → Any
  25. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  26. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  27. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  28. object Matched

Inherited from AnyRef

Inherited from Any

Ungrouped