Logic

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.

6. final class Matched extends AnyRef

Tracks proven atoms in the reverse order they were proved.

Value Members

1. final def !=(arg0: AnyRef): Boolean

Definition Classes
AnyRef
2. final def !=(arg0: Any): Boolean

Definition Classes
Any
3. final def ##(): Int

Definition Classes
AnyRef → Any
4. final def ==(arg0: AnyRef): Boolean

Definition Classes
AnyRef
5. final def ==(arg0: Any): Boolean

Definition Classes
Any

8. def applyAll(cs: Clauses, facts: Set[Literal]): Option[Clauses]

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

Applies known facts to `clause`s, 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

9. final def asInstanceOf[T0]: T0

Definition Classes
Any
10. def atoms(formula: Formula): Set[Atom]

Computes the set of all atoms in `formula`.

11. def atoms(cs: Clauses): Atoms

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

12. def clone(): AnyRef

Attributes
protected[java.lang]
Definition Classes
AnyRef
Annotations
@throws( ... )
13. final def eq(arg0: AnyRef): Boolean

Definition Classes
AnyRef
14. def equals(arg0: Any): Boolean

Definition Classes
AnyRef → Any
15. def finalize(): Unit

Attributes
protected[java.lang]
Definition Classes
AnyRef
Annotations
@throws( classOf[java.lang.Throwable] )
16. final def getClass(): Class[_]

Definition Classes
AnyRef → Any
17. 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()
18. def hashCode(): Int

Definition Classes
AnyRef → Any
19. final def isInstanceOf[T0]: Boolean

Definition Classes
Any
20. final def ne(arg0: AnyRef): Boolean

Definition Classes
AnyRef
21. final def notify(): Unit

Definition Classes
AnyRef
22. final def notifyAll(): Unit

Definition Classes
AnyRef
23. 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.

25. 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()
26. final def synchronized[T0](arg0: ⇒ T0): T0

Definition Classes
AnyRef
27. def toString(): String

Definition Classes
AnyRef → Any
28. final def wait(): Unit

Definition Classes
AnyRef
Annotations
@throws( ... )
29. final def wait(arg0: Long, arg1: Int): Unit

Definition Classes
AnyRef
Annotations
@throws( ... )
30. final def wait(arg0: Long): Unit

Definition Classes
AnyRef
Annotations
@throws( ... )