o

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.

2. final class CyclicNegation extends LogicException
3. final class
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 `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

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)

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

9. def clone()
Attributes
protected[java.lang]
Definition Classes
AnyRef
Annotations
@native() @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
Annotations
@native()
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
Annotations
@native()
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
Annotations
@native()
19. final def notifyAll(): Unit
Definition Classes
AnyRef
Annotations
@native()
20. def reduce(clauses: Clauses, initialFacts: Set[Literal])

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])
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
@native() @throws( ... )
28. object