Compare commits
6 changed files with 222 additions and 439 deletions
74
Main.hs
74
Main.hs
|
|
@ -1,73 +1,27 @@
|
||||||
module Main (main) where
|
module Main (main) where
|
||||||
|
import Prelude (IO, String, getContents, lines, map, print,
|
||||||
import Data.Foldable (Foldable, any)
|
otherwise, Bool(..), filter, id, unlines,
|
||||||
import Data.List (head, tail)
|
mapM_, ($), elem, notElem, (||), putStrLn, read, (.))
|
||||||
import Data.Maybe (isNothing)
|
|
||||||
import GHC.Base (Maybe (..), (==))
|
|
||||||
import System.Environment (getArgs)
|
|
||||||
import Ternary.Statement (Statement (..), st)
|
import Ternary.Statement (Statement (..), st)
|
||||||
import Ternary.Term (Item (..), Term (..))
|
|
||||||
import Ternary.Universum (Universum (..), universum)
|
import Ternary.Universum (Universum (..), universum)
|
||||||
import Ternary.Vee (cleared, hasContradiction, think)
|
import Ternary.Vee (cleared, think)
|
||||||
import Prelude
|
import System.Environment (getArgs)
|
||||||
( Bool (..),
|
import Data.Foldable (Foldable)
|
||||||
IO,
|
|
||||||
String,
|
|
||||||
elem,
|
|
||||||
filter,
|
|
||||||
getContents,
|
|
||||||
id,
|
|
||||||
lines,
|
|
||||||
map,
|
|
||||||
mapM_,
|
|
||||||
notElem,
|
|
||||||
otherwise,
|
|
||||||
print,
|
|
||||||
putStrLn,
|
|
||||||
read,
|
|
||||||
unlines,
|
|
||||||
($),
|
|
||||||
(.),
|
|
||||||
(||),
|
|
||||||
)
|
|
||||||
|
|
||||||
mainSolve :: Universum -> Bool -> IO ()
|
main2 :: Universum -> Bool -> IO ()
|
||||||
mainSolve u onlyNew = do
|
main2 u onlyNew = do
|
||||||
strs <- getContents
|
strs <- getContents
|
||||||
let statements = map str2vee . lines $ strs
|
let statements = map str2vee . lines $ strs
|
||||||
str2vee x = st (read x :: Statement String)
|
str2vee x = st (read x :: Statement String)
|
||||||
mapM_ print
|
mapM_ print
|
||||||
. (if onlyNew then filter (`notElem` statements) else id)
|
. (if onlyNew then filter (`notElem` statements) else id)
|
||||||
. cleared
|
. cleared
|
||||||
. think (universum u)
|
. think (universum u) $ statements
|
||||||
$ statements
|
|
||||||
|
|
||||||
mainProve :: Universum -> Bool -> IO ()
|
|
||||||
mainProve u onlyNew = do
|
|
||||||
strs <- getContents
|
|
||||||
let statements = map str2vee . tail . lines $ strs
|
|
||||||
proveThis = str2vee . head . lines $ strs
|
|
||||||
str2vee x = st (read x :: Statement String)
|
|
||||||
results = cleared . think (universum u) $ statements
|
|
||||||
anyContradictions = any (hasContradiction proveThis) results
|
|
||||||
proof = swapNothingJF $ if anyContradictions then Nothing else Just (Item recalc == Item results)
|
|
||||||
recalc = cleared . think (universum u) $ proveThis : statements
|
|
||||||
swapNothingJF x
|
|
||||||
| isNothing x = Just False
|
|
||||||
| x == Just False = Nothing
|
|
||||||
| x == Just True = Just True
|
|
||||||
|
|
||||||
print recalc
|
|
||||||
putStrLn ""
|
|
||||||
print results
|
|
||||||
putStrLn ""
|
|
||||||
print proof
|
|
||||||
|
|
||||||
withArgs :: (String -> Bool) -> IO ()
|
withArgs :: (String -> Bool) -> IO ()
|
||||||
withArgs a
|
withArgs a
|
||||||
| a "-h" || a "--help" =
|
| a "-h" || a "--help" = putStrLn . unlines $
|
||||||
putStrLn . unlines $
|
["Logical statement solver",
|
||||||
[ "Logical statement solver",
|
|
||||||
"Usage: solver [PARAMETERS]",
|
"Usage: solver [PARAMETERS]",
|
||||||
"",
|
"",
|
||||||
"Designed according to N.P.Brousentsov works",
|
"Designed according to N.P.Brousentsov works",
|
||||||
|
|
@ -82,13 +36,11 @@ withArgs a
|
||||||
"",
|
"",
|
||||||
"A \"Socrates\" \"human\"",
|
"A \"Socrates\" \"human\"",
|
||||||
"",
|
"",
|
||||||
"There are A, E, O, I traditional statements.",
|
"There are A, E, O, I traditional statements exist.",
|
||||||
"Also there are A~, E~, O~, I~ with negated first part"
|
"Also there are A~, E~, O~, I~ with negated first part"
|
||||||
]
|
]
|
||||||
| a "--version" || a "-v" = putStrLn "v1.0.2"
|
| a "--version" || a "-v" = putStrLn "v1.0.2"
|
||||||
| a "--prove" = mainProve Aristotle False
|
| otherwise = main2 uni onlyNew where
|
||||||
| otherwise = mainSolve uni onlyNew
|
|
||||||
where
|
|
||||||
onlyNew = a "--new" || a "-n"
|
onlyNew = a "--new" || a "-n"
|
||||||
uni =
|
uni =
|
||||||
if a "-A" || a "--aristotle"
|
if a "-A" || a "--aristotle"
|
||||||
|
|
|
||||||
144
README.md
144
README.md
|
|
@ -1,143 +1,35 @@
|
||||||
# Deductive Solver
|
# Дедуктивный решатель
|
||||||
|
|
||||||
A *definition* of *x* may be called a rule that divides every existing (and every conceivable) individual object in our world into two parts: those that match the definition *x*, and those that do not, *¬x*.
|
Определением *x* можно называть такое правило, которое делит все существующие (а также мыслимые) индвидуальные предметы в нашем мире на две части: соответствующие определению *x* и не соответствующие *¬x*.
|
||||||
|
|
||||||
While the subject sciences build up a conceptual apparatus, logic studies how concepts relate to one another. Concepts live over the set of all objects under consideration.
|
Тем не менее, если предметные науки формируют понятийный аппарат, то логика изучает соотношения понятий между собой. Понятия существуют на множестве всех рассматриваемых предметов.
|
||||||
|
|
||||||
As the Polish mathematical tradition on the one hand and N. P. Brusentsov on the other rightly point out, the symbol of "existence" of some object, written as ∃, is in fact closely related to disjunction, ∨. Specifically, it is an "integral" disjunction — a disjunction over a set: V*x* means that we run through every object checking it against *x*, and if at least one of them fits, then the set-wide disjunction holds over the whole set as well.
|
Как справедливо отмечает польская математическая традиция с одной стороны и Н.П.Брусенцов с другой стороны, символ "существования" некоторого предмета, записываемый как ∀, на самом деле имеет тесную связь с дизъюнкцией: ∨. Конкретно, это "интегральная" дизъюнкция, дизъюнкция по множеству: Vx значит, что мы пытаемся перебрать все предметы на предмет соответствия x, и если хотя бы один из них подходит, то дизъюнкция по множеству так же существует на всём множестве.
|
||||||
|
|
||||||
By extending sets to three-valued ones — in which an element may be definitely present, definitely absent, or free — we can examine logical concepts in all of their relations.
|
Расширяя множества до нечётких (в которых элементы могут достоверно присутствовать, достоверно отсутствовать и быть свободными), мы можем рассматривать логические понятия во всех их соотношениях.
|
||||||
|
|
||||||
Modern mathematical logic normally combines the features of objects (or anti-features, i.e. failures to match a feature) using Boolean algebra, without three-valued sets. That approach is very successful at describing a single object within a conceptual system fixed in advance. At the same time, it is a poor fit for describing **systems**: more precisely, it forces systems to be described as single objects, which is usually deeply unnatural.
|
Современная математическая логика, как правило, работает совмещением признаков (или анти-признаки, то есть несоответстветствия признакам) предметов булевской алгеброй, без нечётких множеств. Такой подход позволяет достичь больших успехов в описании отдельно взятого предмета в заранее определённой системе понятий. В то же время, такой подход плохо подходит для описания **систем**, точнее, он требует описывать системы как единые предметы, что чаще всего крайне неестественно.
|
||||||
|
|
||||||
The solution is to consider the algebra of three-valued sets over *combinations* of concepts. For example, V*xy* means that somewhere in the set of objects there exists an object combining the features *x* and *y*, whereas V'*xy*' means the opposite: there is no *x* without *y* (which, under additional assumptions, is the relation of entailment).
|
Решением же проблемы является рассмотрение алгебры нечётких множеств относительно комбинаций понятий. К примеру, Vxy означает, что среди всего множества предметов существует предмет, совместивший в себе признаки x и y, а V'xy' напротив, обозначает, что не бывает x без y (что, при дополнительных допущениях, является отношением следования).
|
||||||
|
|
||||||
This idea is discussed in the books of the team that built the "Setun" computer — above all in the books of N. P. Brusentsov. It is presented most fully in his *Foundations of Informatics* (Начала информатики) and *The Art of Reliable Reasoning* (Искусство достоверного рассуждения).
|
Данная концепция упоминается в книгах коллектива авторов, создавших компьютер "Сетунь" - прежде всего, книгах Н.П. Брусенцова. Наиболее полно эта концепция раскрыта в его книгах "Начала информатики" и "Искусство достоверного рассуждения".
|
||||||
|
|
||||||
The deductive solver works with compound logical concepts (for example *xy'z* — an event or object combining *x*, not-*y*, and *z*) and with facts (set-wide disjunctions over such concepts, or negations of those disjunctions).
|
Дедуктивный решатель работает с составными логическими понятиями (например xy'z - это событие или предмет, совместивший в себе x, не-y и z), а также фактами (дизъюнкциями по множеству понятий или отрицаниями этих дизъюнкций).
|
||||||
|
|
||||||
## The four rules (Lewis Carroll's diagram)
|
## 4 правила (диаграмма Льюиса Кэррола)
|
||||||
|
|
||||||
Charles Dodgson, better known as Lewis Carroll, studied questions of logic intensively. He devised a tabular diagram — somewhat reminiscent of a cellular automaton or a game — that allows logical computation to be carried out. Generalizing it, one can state four rules applied to concepts, two of which are "obvious" and two of which create "new" information:
|
Чарльз Доджсон, также известный как Льюис Кэррол, активно исследовал вопросы логики. Он создал диаграмму табличного вида (отчасти напоминающую клеточный автомат или игру), которая позволяет осуществлять логические вычисления. Обобщая, можно сформулировать 4 применяемых к понятиям правила, два из которых "очевидны", а два создают "новую" информацию:
|
||||||
|
|
||||||
1. **Upward truth (obvious).** "If the species V*xyz*' exists, then all of its genera exist: V*x*, V*y*, V*z*', V*xy*, V*xz*', V*yz*' — and moreover the indeterminate something V exists (the wholly unspecific concept)."
|
1. **Восходящая истина (очевидный).** "Если существует вид xyz' (Vxyz'), то существуют все его рода Vx, Vy, Vz', Vxy, Vxz', Vyz', кроме того существует неопределенное нечто V (абсолютно неспецифичное понятие)"
|
||||||
|
|
||||||
2. **Downward falsity (obvious).** "If the genus V'*xy*' does not exist, then none of its species exist either, for example V'*xy*'*z* and V'*xy*'*z*'."
|
2. **Нисходящая ложь (очевидный).** "Если не существует род V'xy', то не существуют никакие его виды, например, V'xy'z, V'xy'z' "
|
||||||
|
|
||||||
3. **Downward truth (new).** "If the genus V*x* exists and the species V'*xy*' does not, then the missing species V*xy* that completes the genus is guaranteed to exist."
|
3. **Нисходящая истина (новый).** "Если существует род Vx и не существует вид V'xy', значит, гарантированно существует дополняющий до рода отсутствующий вид Vxy"
|
||||||
|
|
||||||
4. **Upward falsity (new).** "If both species fail to exist, V'*xy*' and V'*xy*, then the genus V'*x* does not exist either."
|
4. **Восходящая ложь (новый).** "Если оба вида не существуют V'xy' и V'xy, значит, не существует и рода V'x"
|
||||||
|
|
||||||
Applying these rules to the already known facts for as long as any information ("obvious" or "new") keeps being produced, we eventually obtain every logical relation that holds in the system of concepts.
|
Исполняя эти правила над уже известными фактами до тех пор, пока создаётся какая-то информация ("очевидная" либо "новая"), в конечном итоге мы получаем все существующие логические отношения в системе понятий.
|
||||||
|
|
||||||
## On Aristotle's categorical syllogisms
|
## О категорических силлогизмах Аристотеля
|
||||||
|
|
||||||
For Aristotle's traditional categorical syllogisms — and for entailment in the natural-language sense of the word — one must additionally require that every elementary concept is neither empty nor total, that is, that V*x*V*x*'V*y*V*y*'V*z*V*z*' … holds for all concepts *x*, *y*, *z*, …
|
Для традиционных категорических силлогизмов Аристотеля и отношения следования в естественноязыковом смысле этого слова также следует добавлять условие, что любое элементарное понятие не пусто и не полно, то есть, что по всем понятиям *x*, *y*, *z* выполняется VxVx'VyVy'VzVz' ...
|
||||||
|
|
||||||
This is what the `--aristotle` flag does (see below).
|
|
||||||
|
|
||||||
## Building
|
|
||||||
|
|
||||||
The project is plain GHC with no external dependencies; `shell.nix` provides a suitable environment.
|
|
||||||
|
|
||||||
```sh
|
|
||||||
nix-shell # optional, if you use Nix
|
|
||||||
ghc -o solver Main.hs
|
|
||||||
```
|
|
||||||
|
|
||||||
To build the syllogism test runner, compile `Tests/Test.hs` from the project root (it imports the `Ternary.*` modules) and feed it `Tests/syllotest`:
|
|
||||||
|
|
||||||
```sh
|
|
||||||
ghc -i. -o syllotest Tests/Test.hs
|
|
||||||
./syllotest < Tests/syllotest
|
|
||||||
```
|
|
||||||
|
|
||||||
## Usage
|
|
||||||
|
|
||||||
```
|
|
||||||
solver [PARAMETERS]
|
|
||||||
```
|
|
||||||
|
|
||||||
Statements are read from **standard input**, one per line, and results are written to standard output.
|
|
||||||
|
|
||||||
| Parameter | Meaning |
|
|
||||||
| --- | --- |
|
|
||||||
| `-A`, `--aristotle` | Use the Aristotelian universe: assume V*x*V*x*' for every concept *x* mentioned in the input (no concept is empty or total). |
|
|
||||||
| `-n`, `--new` | Print only "new" facts, omitting those that were given in the input. |
|
|
||||||
| `--prove` | Proof mode: check whether the first input line follows from the remaining ones. |
|
|
||||||
| `-h`, `--help` | Show the built-in help. |
|
|
||||||
| `-v`, `--version` | Show the version. |
|
|
||||||
|
|
||||||
Parameters are checked in the order `--help`, `--version`, `--prove`, then normal solving. Note that `--prove` always runs with the Aristotelian universe and ignores `-A` and `-n`.
|
|
||||||
|
|
||||||
### Input format
|
|
||||||
|
|
||||||
Each line is a Haskell-readable value of type `Statement String`:
|
|
||||||
|
|
||||||
```
|
|
||||||
Statement KIND "subject" "predicate"
|
|
||||||
```
|
|
||||||
|
|
||||||
Both terms must be quoted. `KIND` is one of the eight traditional forms — `A`, `E`, `I`, `O` and their primed variants `A'`, `E'`, `I'`, `O'`, in which the *first* term is negated:
|
|
||||||
|
|
||||||
| Kind | Reads as | Equivalent fact |
|
|
||||||
| --- | --- | --- |
|
|
||||||
| `A x y` | Every *x* is *y* | V'*xy*' |
|
|
||||||
| `E x y` | No *x* is *y* | V'*xy* |
|
|
||||||
| `I x y` | Some *x* is *y* | V*xy* |
|
|
||||||
| `O x y` | Some *x* is not *y* | V*xy*' |
|
|
||||||
| `A' x y` | Every non-*x* is *y* | V'*x*'*y*' |
|
|
||||||
| `E' x y` | No non-*x* is *y* | V'*x*'*y* |
|
|
||||||
| `I' x y` | Some non-*x* is *y* | V*x*'*y* |
|
|
||||||
| `O' x y` | Some non-*x* is not *y* | V*x*'*y*' |
|
|
||||||
|
|
||||||
A statement that would place a term and its own negation under the same V — such as `Statement A "x" "x"` — is rejected with an error.
|
|
||||||
|
|
||||||
### Output format
|
|
||||||
|
|
||||||
Facts are printed in Brusentsov's notation, with a **backtick** standing for negation (the `'` used in the prose above):
|
|
||||||
|
|
||||||
- `Vxy` — there exists an object that is both *x* and *y*;
|
|
||||||
- `` V`xy` `` — there exists no object that is *x* but not *y* (i.e. every *x* is *y*);
|
|
||||||
- a backtick immediately after `V` negates the whole set-wide disjunction; a backtick after a term name negates that term.
|
|
||||||
|
|
||||||
### Example: solving
|
|
||||||
|
|
||||||
```sh
|
|
||||||
$ printf 'Statement A "man" "mortal"\nStatement A "Socrates" "man"\n' | ./solver
|
|
||||||
V`manmortal`
|
|
||||||
V`Socratesman`
|
|
||||||
V`mortal`Socrates
|
|
||||||
```
|
|
||||||
|
|
||||||
The third line is the conclusion of the syllogism *Barbara*: there is no non-mortal Socrates — that is, Socrates is mortal.
|
|
||||||
|
|
||||||
With the Aristotelian universe and only the newly derived facts:
|
|
||||||
|
|
||||||
```sh
|
|
||||||
$ printf 'Statement A "man" "mortal"\nStatement A "Socrates" "man"\n' | ./solver -A -n
|
|
||||||
V`mortal`Socrates
|
|
||||||
VmortalmanSocrates
|
|
||||||
VSocrates`man`mortal`
|
|
||||||
```
|
|
||||||
|
|
||||||
### Example: proving
|
|
||||||
|
|
||||||
In `--prove` mode the **first** line is the statement to be proved and the remaining lines are the premises. Three blocks are printed, separated by blank lines: the knowledge derived from the premises *together with* the statement, the knowledge derived from the premises alone, and the verdict.
|
|
||||||
|
|
||||||
```sh
|
|
||||||
$ printf 'Statement A "Socrates" "mortal"\nStatement A "man" "mortal"\nStatement A "Socrates" "man"\n' | ./solver --prove
|
|
||||||
[V`Socratesmortal`,V`manmortal`,V`Socratesman`,VmortalmanSocrates,VSocrates`man`mortal`]
|
|
||||||
|
|
||||||
[V`manmortal`,V`Socratesman`,V`mortal`Socrates,VmortalmanSocrates,VSocrates`man`mortal`]
|
|
||||||
|
|
||||||
Just True
|
|
||||||
```
|
|
||||||
|
|
||||||
The verdict is one of:
|
|
||||||
|
|
||||||
| Verdict | Meaning |
|
|
||||||
| --- | --- |
|
|
||||||
| `Just True` | The statement follows from the premises — adding it yields no new knowledge. |
|
|
||||||
| `Just False` | The statement contradicts the premises. |
|
|
||||||
| `Nothing` | Undetermined: the statement neither follows from nor contradicts the premises. |
|
|
||||||
|
|
@ -1,18 +1,14 @@
|
||||||
module Ternary.Statement (Statement(..), st) where
|
module Ternary.Statement (Statement(..), st) where
|
||||||
import Ternary.Term (Vee, Term(..), Item(..))
|
import Ternary.Term (Vee, Term(..), Item(..))
|
||||||
|
data Statement a = A a a -- Affirmo (general affirmative)
|
||||||
data StatementKind = A | I | E | O | A' | I' | E' | O' deriving (Eq, Show, Read)
|
| I a a -- affIrmo (private affirmative)
|
||||||
data Statement a = Statement StatementKind a a deriving (Eq, Read)
|
| E a a -- nEgo (general negative)
|
||||||
|
| O a a -- negO (private negative)
|
||||||
instance Show a => Show (Statement a) where
|
| A' a a
|
||||||
show (Statement A x y) = "Every " ++ show x ++ " is " ++ show y
|
| I' a a
|
||||||
show (Statement I x y) = "Some of " ++ show x ++ " is " ++ show y
|
| E' a a
|
||||||
show (Statement E x y) = "None of " ++ show x ++ " is " ++ show y
|
| O' a a
|
||||||
show (Statement O x y) = "Some of " ++ show x ++ " isn't " ++ show y
|
deriving (Eq, Show, Read)
|
||||||
show (Statement A' x y) = "Every non-" ++ show x ++ " is " ++ show y
|
|
||||||
show (Statement I' x y) = "Some of non-" ++ show x ++ " is " ++ show y
|
|
||||||
show (Statement E' x y) = "None of non-" ++ show x ++ " is " ++ show y
|
|
||||||
show (Statement O' x y) = "Some of non-" ++ show x ++ " isn't " ++ show y
|
|
||||||
|
|
||||||
inv :: (Eq a) => Term a -> Term a
|
inv :: (Eq a) => Term a -> Term a
|
||||||
inv (Term p x) = Term (not p) x
|
inv (Term p x) = Term (not p) x
|
||||||
|
|
@ -24,11 +20,11 @@ i v x y
|
||||||
| x == y = Term v . Item $ [x]
|
| x == y = Term v . Item $ [x]
|
||||||
|
|
||||||
st :: (Eq a) => Statement a -> Vee a
|
st :: (Eq a) => Statement a -> Vee a
|
||||||
st (Statement A x y) = i False (Term True x) (Term False y)
|
st (A x y) = i False (Term True x) (Term False y)
|
||||||
st (Statement I x y) = i True (Term True x) (Term True y)
|
st (I x y) = i True (Term True x) (Term True y)
|
||||||
st (Statement E x y) = i False (Term True x) (Term True y)
|
st (E x y) = i False (Term True x) (Term True y)
|
||||||
st (Statement O x y) = i True (Term True x) (Term False y)
|
st (O x y) = i True (Term True x) (Term False y)
|
||||||
st (Statement A' x y) = i False (Term False x) (Term False y)
|
st (A' x y) = i False (Term False x) (Term False y)
|
||||||
st (Statement I' x y) = i True (Term False x) (Term True y)
|
st (I' x y) = i True (Term False x) (Term True y)
|
||||||
st (Statement E' x y) = i False (Term False x) (Term True y)
|
st (E' x y) = i False (Term False x) (Term True y)
|
||||||
st (Statement O' x y) = i True (Term False x) (Term False y)
|
st (O' x y) = i True (Term False x) (Term False y)
|
||||||
|
|
|
||||||
140
Ternary/Vee.hs
140
Ternary/Vee.hs
|
|
@ -1,48 +1,10 @@
|
||||||
module Ternary.Vee (isObvious, hasContradiction, newFact, cleared, think) where
|
module Ternary.Vee (isObvious, newFact, cleared, think) where
|
||||||
|
import Data.List (head, intersect, length, nub, null, union, (\\))
|
||||||
import Data.Foldable (concatMap)
|
|
||||||
import Data.List
|
|
||||||
( elem,
|
|
||||||
filter,
|
|
||||||
head,
|
|
||||||
intersect,
|
|
||||||
iterate,
|
|
||||||
length,
|
|
||||||
nub,
|
|
||||||
null,
|
|
||||||
union,
|
|
||||||
(\\),
|
|
||||||
)
|
|
||||||
import Data.Maybe (Maybe (Nothing), mapMaybe)
|
import Data.Maybe (Maybe (Nothing), mapMaybe)
|
||||||
import GHC.Base ((<), (>))
|
import Prelude (Bool (False, True), Eq, any, foldr, fst, map,
|
||||||
import GHC.Maybe (Maybe (..))
|
not, notElem, otherwise, return, snd, ($), (&&),
|
||||||
|
(.), (/=), (<$>), (<*>), (=<<), (==))
|
||||||
import Ternary.Term (Item (..), Term (..), Vee)
|
import Ternary.Term (Item (..), Term (..), Vee)
|
||||||
import Prelude
|
|
||||||
( Bool (False, True),
|
|
||||||
Eq,
|
|
||||||
any,
|
|
||||||
foldr,
|
|
||||||
fst,
|
|
||||||
map,
|
|
||||||
not,
|
|
||||||
notElem,
|
|
||||||
otherwise,
|
|
||||||
return,
|
|
||||||
snd,
|
|
||||||
($),
|
|
||||||
(&&),
|
|
||||||
(.),
|
|
||||||
(/=),
|
|
||||||
(<$>),
|
|
||||||
(<*>),
|
|
||||||
(=<<),
|
|
||||||
(==),
|
|
||||||
)
|
|
||||||
|
|
||||||
type Knowledge a = [Vee a]
|
|
||||||
|
|
||||||
type InferenceRule a = Vee a -> Vee a -> (Knowledge a, Maybe (Vee a))
|
|
||||||
|
|
||||||
isSubsetOf :: (Eq a) => [a] -> [a] -> Bool
|
isSubsetOf :: (Eq a) => [a] -> [a] -> Bool
|
||||||
a `isSubsetOf` b = nda && not ndb
|
a `isSubsetOf` b = nda && not ndb
|
||||||
where
|
where
|
||||||
|
|
@ -55,64 +17,52 @@ isObvious (Term x (Item a)) (Term y (Item b))
|
||||||
| x = a `isSubsetOf` b
|
| x = a `isSubsetOf` b
|
||||||
| not x = b `isSubsetOf` a
|
| not x = b `isSubsetOf` a
|
||||||
|
|
||||||
hasContradiction :: (Eq a) => Vee a -> Vee a -> Bool
|
newFact :: (Eq a) => Vee a -> Vee a -> ([Vee a], Maybe (Vee a))
|
||||||
hasContradiction (Term x (Item a)) (Term y (Item b))
|
|
||||||
| a == b && x /= y = True
|
|
||||||
| a `isSubsetOf` b && x < y = True
|
|
||||||
| b `isSubsetOf` a && x > y = True
|
|
||||||
| otherwise = False
|
|
||||||
|
|
||||||
notT :: Term a -> Term a
|
|
||||||
notT (Term x v) = Term (not x) v
|
|
||||||
|
|
||||||
rulePosFromNeg :: (Eq a) => InferenceRule a
|
|
||||||
rulePosFromNeg (Term False (Item negSet)) positive@(Term True (Item posSet))
|
|
||||||
| length diff /= 1 = ([], Nothing)
|
|
||||||
| missing `elem` posSet = ([], Nothing)
|
|
||||||
| otherwise = ([positive], Just (Term True (Item (missing : posSet))))
|
|
||||||
where
|
|
||||||
diff = negSet \\ posSet
|
|
||||||
missing = notT (head diff)
|
|
||||||
|
|
||||||
ruleNegFromNeg :: (Eq a) => InferenceRule a
|
|
||||||
ruleNegFromNeg (Term False (Item i0)) (Term False (Item i1))
|
|
||||||
| length evidence /= 1 = ([], Nothing)
|
|
||||||
| null diff0 && null diff1 = (map (Term False . Item) [i0, i1], Just (Term False (Item result)))
|
|
||||||
| otherwise = ([], Just (Term False (Item result)))
|
|
||||||
where
|
|
||||||
evidence = map notT i0 `intersect` i1
|
|
||||||
diff0 = (i0 \\ i1) \\ map notT evidence
|
|
||||||
diff1 = (i1 \\ i0) \\ evidence
|
|
||||||
result = (i0 `intersect` i1) `union` diff0 `union` diff1
|
|
||||||
|
|
||||||
newFact :: (Eq a) => InferenceRule a
|
|
||||||
newFact a@(Term True _) b@(Term False _) = newFact b a
|
newFact a@(Term True _) b@(Term False _) = newFact b a
|
||||||
newFact a@(Term False _) b@(Term True _) = rulePosFromNeg a b
|
newFact (Term False (Item iF)) tT@(Term True (Item iT))
|
||||||
newFact a@(Term False _) b@(Term False _) = ruleNegFromNeg a b
|
| length ldF /= 1 = ([], Nothing)
|
||||||
|
| otherwise =
|
||||||
|
if d'F `notElem` iT
|
||||||
|
then (return tT, return (Term True (Item (d'F:iT))))
|
||||||
|
else ([], Nothing)
|
||||||
|
where
|
||||||
|
ldF = iF \\ iT
|
||||||
|
d'F = notT . head $ ldF
|
||||||
|
notT (Term x v) = Term (not x) v
|
||||||
|
newFact (Term False (Item i0)) (Term False (Item i1))
|
||||||
|
| length e /= 1 = ([], Nothing)
|
||||||
|
| otherwise =
|
||||||
|
if null d0 && null d1
|
||||||
|
then (map (Term False . Item) [i0, i1], vee0)
|
||||||
|
else ([], vee0)
|
||||||
|
where
|
||||||
|
notT (Term x v) = Term (not x) v
|
||||||
|
terms = (i0 `intersect` i1) `union` d0 `union` d1
|
||||||
|
e = map notT i0 `intersect` i1
|
||||||
|
d0 = (i0 \\ i1) \\ map notT e
|
||||||
|
d1 = (i1 \\ i0) \\ e
|
||||||
|
vee0 = return (Term False (Item terms))
|
||||||
newFact _ _ = ([], Nothing)
|
newFact _ _ = ([], Nothing)
|
||||||
|
|
||||||
next :: (Eq a) => (Knowledge a, Knowledge a) -> (Knowledge a, Knowledge a)
|
pseudofix :: (Eq a) => (a -> a) -> a -> a
|
||||||
next (old, new) = (old `union` new \\ used, added)
|
pseudofix f x0
|
||||||
|
| y == y' = y
|
||||||
|
| otherwise = y'
|
||||||
where
|
where
|
||||||
results = [newFact o n | o <- old, n <- new]
|
y = f x0
|
||||||
used = concatMap fst results
|
y' = f y
|
||||||
added = mapMaybe snd results
|
|
||||||
|
|
||||||
applyFacts :: (Eq a) => Knowledge a -> Knowledge a -> Knowledge a
|
next :: (Eq a) => ([Vee a], [Vee a]) -> ([Vee a], [Vee a])
|
||||||
applyFacts old new =
|
next (o,n) = (o `union` n \\ (fst =<< r), mapMaybe snd r)
|
||||||
fst . head . dropStable $ iterate next (old, new)
|
|
||||||
where
|
where
|
||||||
dropStable (x : y : xs)
|
r = newFact <$> o <*> n
|
||||||
| x == y = [x]
|
|
||||||
| otherwise = dropStable (y : xs)
|
|
||||||
dropStable _ = []
|
|
||||||
|
|
||||||
cleared :: (Eq a) => Knowledge a -> Knowledge a
|
applyFacts :: (Eq a) => [Vee a] -> [Vee a] -> [Vee a]
|
||||||
cleared vees = nub $ filter (not . isRedundant) vees
|
applyFacts old new = fst $ pseudofix next (old, new)
|
||||||
where
|
|
||||||
isRedundant v = any (isObvious v) vees
|
|
||||||
|
|
||||||
think :: (Eq a) => (Knowledge a -> Knowledge a) -> Knowledge a -> Knowledge a
|
cleared :: (Eq a) => [Vee a] -> [Vee a]
|
||||||
think addition = foldr (applyFacts . withUni . return) []
|
cleared vees = nub [vee | vee <- vees, not $ any (isObvious vee) vees]
|
||||||
where
|
|
||||||
|
think :: (Eq a) => ([Vee a]->[Vee a]) -> [Vee a] -> [Vee a]
|
||||||
|
think addition = foldr (applyFacts . withUni . return) [] where
|
||||||
withUni vees = applyFacts (addition vees) vees
|
withUni vees = applyFacts (addition vees) vees
|
||||||
|
|
|
||||||
192
Tests/syllotest
192
Tests/syllotest
|
|
@ -1,96 +1,96 @@
|
||||||
(Statement A "y" "z", Statement A "x" "y", Statement A "x" "z")
|
(A "y" "z", A "x" "y", A "x" "z")
|
||||||
(Statement A "y" "z", Statement E' "x" "y", Statement E' "x" "z")
|
(A "y" "z", E' "x" "y", E' "x" "z")
|
||||||
(Statement E "y" "z", Statement A "x" "y", Statement E "x" "z")
|
(E "y" "z", A "x" "y", E "x" "z")
|
||||||
(Statement E "y" "z", Statement E' "x" "y", Statement A' "x" "z")
|
(E "y" "z", E' "x" "y", A' "x" "z")
|
||||||
(Statement A "y" "z", Statement A "x" "y", Statement I "x" "z")
|
(A "y" "z", A "x" "y", I "x" "z")
|
||||||
(Statement A "y" "z", Statement A "x" "y", Statement I' "x" "z")
|
(A "y" "z", A "x" "y", I' "x" "z")
|
||||||
(Statement A "y" "z", Statement E' "x" "y", Statement O "x" "z")
|
(A "y" "z", E' "x" "y", O "x" "z")
|
||||||
(Statement A "y" "z", Statement E' "x" "y", Statement O' "x" "z")
|
(A "y" "z", E' "x" "y", O' "x" "z")
|
||||||
(Statement E "y" "z", Statement A "x" "y", Statement O "x" "z")
|
(E "y" "z", A "x" "y", O "x" "z")
|
||||||
(Statement E "y" "z", Statement A "x" "y", Statement O' "x" "z")
|
(E "y" "z", A "x" "y", O' "x" "z")
|
||||||
(Statement E "y" "z", Statement E' "x" "y", Statement I "x" "z")
|
(E "y" "z", E' "x" "y", I "x" "z")
|
||||||
(Statement E "y" "z", Statement E' "x" "y", Statement I' "x" "z")
|
(E "y" "z", E' "x" "y", I' "x" "z")
|
||||||
(Statement A "y" "z", Statement A' "x" "y", Statement I "x" "z")
|
(A "y" "z", A' "x" "y", I "x" "z")
|
||||||
(Statement A "y" "z", Statement E "x" "y", Statement O' "x" "z")
|
(A "y" "z", E "x" "y", O' "x" "z")
|
||||||
(Statement E "y" "z", Statement A' "x" "y", Statement O "x" "z")
|
(E "y" "z", A' "x" "y", O "x" "z")
|
||||||
(Statement E "y" "z", Statement E "x" "y", Statement I' "x" "z")
|
(E "y" "z", E "x" "y", I' "x" "z")
|
||||||
(Statement A "y" "z", Statement I "x" "y", Statement I "x" "z")
|
(A "y" "z", I "x" "y", I "x" "z")
|
||||||
(Statement A "y" "z", Statement O' "x" "y", Statement O' "x" "z")
|
(A "y" "z", O' "x" "y", O' "x" "z")
|
||||||
(Statement E "y" "z", Statement I "x" "y", Statement O "x" "z")
|
(E "y" "z", I "x" "y", O "x" "z")
|
||||||
(Statement E "y" "z", Statement O' "x" "y", Statement I' "x" "z")
|
(E "y" "z", O' "x" "y", I' "x" "z")
|
||||||
(Statement I "y" "z", Statement A' "x" "y", Statement I "x" "z")
|
(I "y" "z", A' "x" "y", I "x" "z")
|
||||||
(Statement I "y" "z", Statement E "x" "y", Statement O' "x" "z")
|
(I "y" "z", E "x" "y", O' "x" "z")
|
||||||
(Statement O "y" "z", Statement A' "x" "y", Statement O "x" "z")
|
(O "y" "z", A' "x" "y", O "x" "z")
|
||||||
(Statement O "y" "z", Statement E "x" "y", Statement I' "x" "z")
|
(O "y" "z", E "x" "y", I' "x" "z")
|
||||||
(Statement A "z" "y", Statement A' "x" "y", Statement A' "x" "z")
|
(A "z" "y", A' "x" "y", A' "x" "z")
|
||||||
(Statement A "z" "y", Statement E "x" "y", Statement E "x" "z")
|
(A "z" "y", E "x" "y", E "x" "z")
|
||||||
(Statement E "z" "y", Statement A "x" "y", Statement E "x" "z")
|
(E "z" "y", A "x" "y", E "x" "z")
|
||||||
(Statement E "z" "y", Statement E' "x" "y", Statement A' "x" "z")
|
(E "z" "y", E' "x" "y", A' "x" "z")
|
||||||
(Statement A "z" "y", Statement A' "x" "y", Statement I "x" "z")
|
(A "z" "y", A' "x" "y", I "x" "z")
|
||||||
(Statement A "z" "y", Statement A' "x" "y", Statement I' "x" "z")
|
(A "z" "y", A' "x" "y", I' "x" "z")
|
||||||
(Statement A "z" "y", Statement E "x" "y", Statement O "x" "z")
|
(A "z" "y", E "x" "y", O "x" "z")
|
||||||
(Statement A "z" "y", Statement E "x" "y", Statement O' "x" "z")
|
(A "z" "y", E "x" "y", O' "x" "z")
|
||||||
(Statement E "z" "y", Statement A "x" "y", Statement O "x" "z")
|
(E "z" "y", A "x" "y", O "x" "z")
|
||||||
(Statement E "z" "y", Statement A "x" "y", Statement O' "x" "z")
|
(E "z" "y", A "x" "y", O' "x" "z")
|
||||||
(Statement E "z" "y", Statement E' "x" "y", Statement I "x" "z")
|
(E "z" "y", E' "x" "y", I "x" "z")
|
||||||
(Statement E "z" "y", Statement E' "x" "y", Statement I' "x" "z")
|
(E "z" "y", E' "x" "y", I' "x" "z")
|
||||||
(Statement A "z" "y", Statement A "x" "y", Statement I' "x" "z")
|
(A "z" "y", A "x" "y", I' "x" "z")
|
||||||
(Statement A "z" "y", Statement E' "x" "y", Statement O "x" "z")
|
(A "z" "y", E' "x" "y", O "x" "z")
|
||||||
(Statement E "z" "y", Statement A' "x" "y", Statement O "x" "z")
|
(E "z" "y", A' "x" "y", O "x" "z")
|
||||||
(Statement E "z" "y", Statement E "x" "y", Statement I' "x" "z")
|
(E "z" "y", E "x" "y", I' "x" "z")
|
||||||
(Statement A "z" "y", Statement I' "x" "y", Statement I' "x" "z")
|
(A "z" "y", I' "x" "y", I' "x" "z")
|
||||||
(Statement A "z" "y", Statement O "x" "y", Statement O "x" "z")
|
(A "z" "y", O "x" "y", O "x" "z")
|
||||||
(Statement E "z" "y", Statement I "x" "y", Statement O "x" "z")
|
(E "z" "y", I "x" "y", O "x" "z")
|
||||||
(Statement E "z" "y", Statement O' "x" "y", Statement I' "x" "z")
|
(E "z" "y", O' "x" "y", I' "x" "z")
|
||||||
(Statement I "z" "y", Statement A' "x" "y", Statement I "x" "z")
|
(I "z" "y", A' "x" "y", I "x" "z")
|
||||||
(Statement I "z" "y", Statement E "x" "y", Statement O' "x" "z")
|
(I "z" "y", E "x" "y", O' "x" "z")
|
||||||
(Statement O "z" "y", Statement A "x" "y", Statement O' "x" "z")
|
(O "z" "y", A "x" "y", O' "x" "z")
|
||||||
(Statement O "z" "y", Statement E' "x" "y", Statement I "x" "z")
|
(O "z" "y", E' "x" "y", I "x" "z")
|
||||||
(Statement A "y" "z", Statement A' "y" "x", Statement A "x" "z")
|
(A "y" "z", A' "y" "x", A "x" "z")
|
||||||
(Statement A "y" "z", Statement E' "y" "x", Statement E' "x" "z")
|
(A "y" "z", E' "y" "x", E' "x" "z")
|
||||||
(Statement E "y" "z", Statement A' "y" "x", Statement E "x" "z")
|
(E "y" "z", A' "y" "x", E "x" "z")
|
||||||
(Statement E "y" "z", Statement E' "y" "x", Statement A' "x" "z")
|
(E "y" "z", E' "y" "x", A' "x" "z")
|
||||||
(Statement A "y" "z", Statement A' "y" "x", Statement I "x" "z")
|
(A "y" "z", A' "y" "x", I "x" "z")
|
||||||
(Statement A "y" "z", Statement A' "y" "x", Statement I' "x" "z")
|
(A "y" "z", A' "y" "x", I' "x" "z")
|
||||||
(Statement A "y" "z", Statement E' "y" "x", Statement O "x" "z")
|
(A "y" "z", E' "y" "x", O "x" "z")
|
||||||
(Statement A "y" "z", Statement E' "y" "x", Statement O' "x" "z")
|
(A "y" "z", E' "y" "x", O' "x" "z")
|
||||||
(Statement E "y" "z", Statement A' "y" "x", Statement O "x" "z")
|
(E "y" "z", A' "y" "x", O "x" "z")
|
||||||
(Statement E "y" "z", Statement A' "y" "x", Statement O' "x" "z")
|
(E "y" "z", A' "y" "x", O' "x" "z")
|
||||||
(Statement E "y" "z", Statement E' "y" "x", Statement I "x" "z")
|
(E "y" "z", E' "y" "x", I "x" "z")
|
||||||
(Statement E "y" "z", Statement E' "y" "x", Statement I' "x" "z")
|
(E "y" "z", E' "y" "x", I' "x" "z")
|
||||||
(Statement A "y" "z", Statement A "y" "x", Statement I "x" "z")
|
(A "y" "z", A "y" "x", I "x" "z")
|
||||||
(Statement A "y" "z", Statement E "y" "x", Statement O' "x" "z")
|
(A "y" "z", E "y" "x", O' "x" "z")
|
||||||
(Statement E "y" "z", Statement A "y" "x", Statement O "x" "z")
|
(E "y" "z", A "y" "x", O "x" "z")
|
||||||
(Statement E "y" "z", Statement E "y" "x", Statement I' "x" "z")
|
(E "y" "z", E "y" "x", I' "x" "z")
|
||||||
(Statement A "y" "z", Statement I "y" "x", Statement I "x" "z")
|
(A "y" "z", I "y" "x", I "x" "z")
|
||||||
(Statement A "y" "z", Statement O "y" "x", Statement O' "x" "z")
|
(A "y" "z", O "y" "x", O' "x" "z")
|
||||||
(Statement E "y" "z", Statement I "y" "x", Statement O "x" "z")
|
(E "y" "z", I "y" "x", O "x" "z")
|
||||||
(Statement E "y" "z", Statement O "y" "x", Statement I' "x" "z")
|
(E "y" "z", O "y" "x", I' "x" "z")
|
||||||
(Statement I "y" "z", Statement A "y" "x", Statement I "x" "z")
|
(I "y" "z", A "y" "x", I "x" "z")
|
||||||
(Statement I "y" "z", Statement E "y" "x", Statement O' "x" "z")
|
(I "y" "z", E "y" "x", O' "x" "z")
|
||||||
(Statement O "y" "z", Statement A "y" "x", Statement O "x" "z")
|
(O "y" "z", A "y" "x", O "x" "z")
|
||||||
(Statement O "y" "z", Statement E "y" "x", Statement I' "x" "z")
|
(O "y" "z", E "y" "x", I' "x" "z")
|
||||||
(Statement A "z" "y", Statement A "y" "x", Statement A' "x" "z")
|
(A "z" "y", A "y" "x", A' "x" "z")
|
||||||
(Statement A "z" "y", Statement E "y" "x", Statement E "x" "z")
|
(A "z" "y", E "y" "x", E "x" "z")
|
||||||
(Statement E "z" "y", Statement A' "y" "x", Statement E "x" "z")
|
(E "z" "y", A' "y" "x", E "x" "z")
|
||||||
(Statement E "z" "y", Statement E' "y" "x", Statement A' "x" "z")
|
(E "z" "y", E' "y" "x", A' "x" "z")
|
||||||
(Statement A "z" "y", Statement A "y" "x", Statement I "x" "z")
|
(A "z" "y", A "y" "x", I "x" "z")
|
||||||
(Statement A "z" "y", Statement A "y" "x", Statement I' "x" "z")
|
(A "z" "y", A "y" "x", I' "x" "z")
|
||||||
(Statement A "z" "y", Statement E "y" "x", Statement O "x" "z")
|
(A "z" "y", E "y" "x", O "x" "z")
|
||||||
(Statement A "z" "y", Statement E "y" "x", Statement O' "x" "z")
|
(A "z" "y", E "y" "x", O' "x" "z")
|
||||||
(Statement E "z" "y", Statement A' "y" "x", Statement O "x" "z")
|
(E "z" "y", A' "y" "x", O "x" "z")
|
||||||
(Statement E "z" "y", Statement A' "y" "x", Statement O' "x" "z")
|
(E "z" "y", A' "y" "x", O' "x" "z")
|
||||||
(Statement E "z" "y", Statement E' "y" "x", Statement I "x" "z")
|
(E "z" "y", E' "y" "x", I "x" "z")
|
||||||
(Statement E "z" "y", Statement E' "y" "x", Statement I' "x" "z")
|
(E "z" "y", E' "y" "x", I' "x" "z")
|
||||||
(Statement A "z" "y", Statement A' "y" "x", Statement I' "x" "z")
|
(A "z" "y", A' "y" "x", I' "x" "z")
|
||||||
(Statement A "z" "y", Statement E' "y" "x", Statement O "x" "z")
|
(A "z" "y", E' "y" "x", O "x" "z")
|
||||||
(Statement E "z" "y", Statement A "y" "x", Statement O "x" "z")
|
(E "z" "y", A "y" "x", O "x" "z")
|
||||||
(Statement E "z" "y", Statement E "y" "x", Statement I' "x" "z")
|
(E "z" "y", E "y" "x", I' "x" "z")
|
||||||
(Statement A "z" "y", Statement I' "y" "x", Statement I' "x" "z")
|
(A "z" "y", I' "y" "x", I' "x" "z")
|
||||||
(Statement A "z" "y", Statement O' "y" "x", Statement O "x" "z")
|
(A "z" "y", O' "y" "x", O "x" "z")
|
||||||
(Statement E "z" "y", Statement I "y" "x", Statement O "x" "z")
|
(E "z" "y", I "y" "x", O "x" "z")
|
||||||
(Statement E "z" "y", Statement O "y" "x", Statement I' "x" "z")
|
(E "z" "y", O "y" "x", I' "x" "z")
|
||||||
(Statement I "z" "y", Statement A "y" "x", Statement I "x" "z")
|
(I "z" "y", A "y" "x", I "x" "z")
|
||||||
(Statement I "z" "y", Statement E "y" "x", Statement O' "x" "z")
|
(I "z" "y", E "y" "x", O' "x" "z")
|
||||||
(Statement O "z" "y", Statement A' "y" "x", Statement O' "x" "z")
|
(O "z" "y", A' "y" "x", O' "x" "z")
|
||||||
(Statement O "z" "y", Statement E' "y" "x", Statement I "x" "z")
|
(O "z" "y", E' "y" "x", I "x" "z")
|
||||||
|
|
|
||||||
|
|
@ -1,7 +0,0 @@
|
||||||
{ pkgs ? import <nixpkgs> {} }:
|
|
||||||
|
|
||||||
pkgs.mkShell {
|
|
||||||
buildInputs = with pkgs; [
|
|
||||||
ghc
|
|
||||||
];
|
|
||||||
}
|
|
||||||
Loading…
Reference in a new issue