Crete is a DSL in the Scala programming language for logic inference. With Crete, you can write first-order logic sentences naturally, as you would write them by hand.
Write sentences in first order logic in the most intuitive way:
∀('p)('smokes('p) & !'drinks('p) → 'cancer('p))
Creating a knowledge base on which various kinds of queries can be performed:
val kb = Set[Sentence](
∀('p)('smokes('p) implies 'cancer('p)),
∀('p)('cancer('x) implies 'dies('p)),
'smokes("john"),
'smokes("mary")
)
val query1 = kb entails 'dies("john")
val query2 = 'dies("john") follows kb
val query3 = kb existentialQuery ∃('x)('smokes('x))
The default algorithm used for entailment inference is refutation resolution. You can change this to one of other available presets like forward chaining, etc., or you can make your own inference algorithm by conforming to the typeclass TODO
. As an example, an inference algorithm that provides trivially a believe-in-everything-inference can be written as:
TODO
- CreteSoft: a probabilistic soft logic framwork built upon Crete.
- CreteMarkov: a Markov logic network framework built upon Crete.