object Logic
- Alphabetic
- By Inheritance
- Logic
- AnyRef
- Any
- Hide All
- Show All
- Public
- All
Type Members
-
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.
- final class CyclicNegation extends LogicException
- final class InitialContradictions extends LogicException
- final class InitialOverlap extends LogicException
- sealed abstract class LogicException extends AnyRef
-
final
class
Matched extends AnyRef
Tracks proven atoms in the reverse order they were proved.
Value Members
-
final
def
!=(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
final
def
##(): Int
- Definition Classes
- AnyRef → Any
-
final
def
==(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- def applyAll(c: Clause, facts: Set[Literal]): Option[Clause]
-
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 infacts
is present in the result Postcondition: No clauses have an empty head -
final
def
asInstanceOf[T0]: T0
- Definition Classes
- Any
-
def
atoms(formula: Formula): Set[Atom]
Computes the set of all atoms in
formula
. -
def
atoms(cs: Clauses): Atoms
Computes the atoms in the heads and bodies of the clauses in
clause
. -
def
clone(): AnyRef
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws( ... ) @native()
-
final
def
eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
-
def
equals(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
def
finalize(): Unit
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws( classOf[java.lang.Throwable] )
-
final
def
getClass(): Class[_]
- Definition Classes
- AnyRef → Any
- Annotations
- @native()
-
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 returnList(a, d)
: a :- b, not c d :- a- Annotations
- @tailrec()
-
def
hashCode(): Int
- Definition Classes
- AnyRef → Any
- Annotations
- @native()
-
final
def
isInstanceOf[T0]: Boolean
- Definition Classes
- Any
-
final
def
ne(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
-
final
def
notify(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native()
-
final
def
notifyAll(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native()
-
def
reduce(clauses: Clauses, initialFacts: Set[Literal]): Either[LogicException, Matched]
Computes the variables in the unique stable model for the program represented by
clauses
andinitialFacts
.Computes the variables in the unique stable model for the program represented by
clauses
andinitialFacts
.clause
may not have any negative feedback (that is, negation is acyclic) andinitialFacts
cannot be in the head of any clauses inclause
. These restrictions ensure that the logic program has a unique minimal model. - def reduceAll(clauses: List[Clause], initialFacts: Set[Literal]): Either[LogicException, Matched]
-
def
substitute(formula: Formula, facts: Set[Literal]): Option[Formula]
Derives the formula that results from substituting
facts
intoformula
.Derives the formula that results from substituting
facts
intoformula
.- Annotations
- @tailrec()
-
final
def
synchronized[T0](arg0: ⇒ T0): T0
- Definition Classes
- AnyRef
-
def
toString(): String
- Definition Classes
- AnyRef → Any
-
final
def
wait(): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws( ... )
-
final
def
wait(arg0: Long, arg1: Int): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws( ... )
-
final
def
wait(arg0: Long): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws( ... ) @native()
- object Matched