The Final Pathetic Bleatings of the Forum

Question:

Would you please demonstrate to those people too lazy to
read the documentation on Lambek calculi and connectionist
search algorithms how your system works by solving a very
simple logic problem? Would you please show how the
questions are translated into Lambek calculi, the quadratic
search algorithm implementation of connectionist search
algoritms use the Lambek calculi translation of the
question, and the translation from Lambek calculi into
English for the search results? Please use the following
example:

All dogs have wet noses.
Rover is a dog.
Would you please prove that Rover has a wet nose.

Replies:

C'mon Clara, let's go pee.

In order for you to understand the last reply of this question, you need to read the following definitions of the formal system first.

```%%% Admissibility of Cut in Intuitionistic Sequent Calculusca : {A:o} conc A -> (hyp A -> conc C) -> conc C -> type.%% Axiom Conversionsca_axiom_l : ca A (axiom H) E (E H).ca_axiom_r : ca A D ([h:hyp A] axiom h) D.%% Essential Conversionsca_and1 : ca (A1 and A2) (andr D1 D2)
([h:hyp (A1 and A2)] andl1 (E1 h) h) F
<- ({h1:hyp A1}
ca (A1 and A2) (andr D1 D2)
([h:hyp (A1 and A2)] E1 h h1) (E1' h1))
<- ca A1 D1 E1' F.ca_and2 : ca (A1 and A2) (andr D1 D2)
([h:hyp (A1 and A2)] andl2 (E2 h) h) F
<- ({h2:hyp A2}
ca (A1 and A2) (andr D1 D2)
([h:hyp (A1 and A2)] E2 h h2) (E2' h2))
<- ca A2 D2 E2' F.ca_imp  : ca (A1 imp A2) (impr D2)
([h:hyp (A1 imp A2)] impl (E1 h) (E2 h) h) F
<- ca (A1 imp A2) (impr D2) E1 E1'
<- ({h2:hyp A2}
ca (A1 imp A2) (impr D2)
([h:hyp (A1 imp A2)] E2 h h2) (E2' h2))
<- ca A1 E1' D2 D2'
<- ca A2 D2' E2' F.ca_or1  : ca (A1 or A2) (orr1 D1)
([h:hyp (A1 or A2)] orl (E1 h) (E2 h) h) F
<- ({h1:hyp A1}
ca (A1 or A2) (orr1 D1)
([h:hyp (A1 or A2)] E1 h h1) (E1' h1))
<- ca A1 D1 E1' F.ca_or2  : ca (A1 or A2) (orr2 D2)
([h:hyp (A1 or A2)] orl (E1 h) (E2 h) h) F
<- ({h2:hyp A2}
ca (A1 or A2) (orr2 D2)
([h:hyp (A1 or A2)] E2 h h2) (E2' h2))
<- ca A2 D2 E2' F.ca_not  : ca (not A1) (notr D1)
([h:hyp (not A1)] notl (E1 h) h) (F2 C)
<- ca (not A1) (notr D1) E1 F1
<- ({p:o} ca A1 F1 ([h1:hyp A1] D1 p h1) (F2 p)).ca_forall : ca (forall A1) (forallr D1)
([h:hyp (forall A1)] foralll T (E1 h) h) F
<- ({h2:hyp (A1 T)}
ca (forall A1) (forallr D1)
([h:hyp (forall A1)] E1 h h2) (E1' h2))
<- ca (A1 T) (D1 T) E1' F.ca_exists : ca (exists A1) (existsr T D1)
([h:hyp (exists A1)] existsl (E1 h) h) F
<- ({a:i} {h1:hyp (A1 a)}
ca (exists A1) (existsr T D1)
([h:hyp (exists A1)] E1 h a h1) (E1' a h1))
<- ca (A1 T) D1 (E1' T) F.%% Left Commutative Conversionscal_andl1  : ca A (andl1 D1 H) E (andl1 D1' H)
<- {h1:hyp B1} ca A (D1 h1) E (D1' h1).cal_andl2  : ca A (andl2 D2 H) E (andl2 D2' H)
<- {h2:hyp B2} ca A (D2 h2) E (D2' h2).cal_impl   : ca A (impl D1 D2 H) E (impl D1 D2' H)
<- ({h2:hyp B2} ca A (D2 h2) E (D2' h2)).cal_orl    : ca A (orl D1 D2 H) E (orl D1' D2' H)
<- ({h1:hyp B1} ca A (D1 h1) E (D1' h1))
<- ({h2:hyp B2} ca A (D2 h2) E (D2' h2)).cal_notl   : ca A (notl D1 H) E (notl D1 H).cal_falsel  : ca A (falsel H) E (falsel H).cal_foralll : ca A (foralll T D1 H) E (foralll T D1' H)
<- ({h} ca A (D1 h) E (D1' h)).cal_existsl : ca A (existsl D1 H) E (existsl D1' H)
<- ({a:i} {h:hyp (B1 a)}
ca A (D1 a h) E (D1' a h)).%% Right Commutative Conversionscar_axiom : ca A D ([h:hyp A] axiom H1) (axiom H1).car_andr : ca A D ([h:hyp A] andr (E1 h) (E2 h)) (andr E1' E2')
<- ca A D E1 E1'
<- ca A D E2 E2'.car_andl1: ca A D ([h:hyp A] andl1 (E1 h) H) (andl1 E1' H)
<- ({h1:hyp B1} ca A D ([h:hyp A] E1 h h1) (E1' h1)).car_andl2: ca A D ([h:hyp A] andl2 (E2 h) H) (andl2 E2' H)
<- ({h2:hyp B2} ca A D ([h:hyp A] E2 h h2) (E2' h2)).car_impr : ca A D ([h:hyp A] impr (E2 h)) (impr E2')
<- ({h1:hyp B1} ca A D ([h:hyp A] E2 h h1) (E2' h1)).car_impl : ca A D ([h:hyp A] impl (E1 h) (E2 h) H) (impl E1' E2' H)
<- ca A D E1 E1'
<- ({h2:hyp B2} ca A D ([h:hyp A] E2 h h2) (E2' h2)).car_orr1 : ca A D ([h:hyp A] orr1 (E1 h)) (orr1 E1')
<- ca A D E1 E1'.car_orr2 : ca A D ([h:hyp A] orr2 (E2 h)) (orr2 E2')
<- ca A D E2 E2'.car_orl  : ca A D ([h:hyp A] orl (E1 h) (E2 h) H) (orl E1' E2' H)
<- ({h1:hyp B1} ca A D ([h:hyp A] E1 h h1) (E1' h1))
<- ({h2:hyp B2} ca A D ([h:hyp A] E2 h h2) (E2' h2)).car_notr : ca A D ([h:hyp A] notr (E1 h)) (notr E1')
<- ({p:o} {h1:hyp B1} ca A D ([h:hyp A] E1 h p h1) (E1' p h1)).car_notl : ca A D ([h:hyp A] notl (E1 h) H) (notl E1' H)
<- ca A D E1 E1'.car_truer: ca A D ([h:hyp A] truer) (truer).car_falsel : ca A D ([h:hyp A] falsel H) (falsel H).car_forallr : ca A D ([h:hyp A] forallr (E1 h)) (forallr E1')
<- ({a:i} ca A D ([h:hyp A] E1 h a) (E1' a)).car_foralll: ca A D ([h:hyp A] foralll T (E1 h) H) (foralll T E1' H)
<- ({h1} ca A D ([h:hyp A] E1 h h1) (E1' h1)).car_existsr : ca A D ([h:hyp A] existsr T (E1 h)) (existsr T E1')
<- ca A D E1 E1'.car_existsl : ca A D ([h:hyp A] existsl (E1 h) H) (existsl E1' H)
<- ({a:i} {h1:hyp (B1 a)}
ca A D ([h:hyp A] E1 h a h1) (E1' a h1)).```

```%%% Cut-Free Classical Sequent Calculus# : type.         % Token (for contradiction)
neg : o -> type.  % Hypotheses (left)
pos : o -> type.  % Conclusions (right)
%name # D
%name neg N
%name pos Paxiom' : (neg A -> pos A -> #).andr'  : (pos A -> #)
-> (pos B -> #)
-> (pos (A and B) -> #).andl1' : (neg A -> #)
-> (neg (A and B) -> #).andl2' : (neg B -> #)
-> (neg (A and B) -> #).impr'  : (neg A -> pos B -> #)
-> (pos (A imp B) -> #).impl'  : (pos A -> #)
-> (neg B -> #)
-> (neg (A imp B) -> #).orr1'  : (pos A -> #)
-> (pos (A or B) -> #).orr2'  : (pos B -> #)
-> (pos (A or B) -> #).orl'   : (neg A -> #)
-> (neg B -> #)
-> (neg (A or B) -> #).notr'  : (neg A -> #)
-> (pos (not A) -> #).notl'  : (pos A -> #)
-> (neg (not A) -> #).truer' : (pos (true) -> #).falsel' : (neg (false) -> #).forallr' : ({a:i} pos (A a) -> #)
-> (pos (forall A) -> #). foralll' : {T:i} (neg (A T) -> #)
-> (neg (forall A) -> #).existsr' : {T:i} (pos (A T) -> #)
-> (pos (exists A) -> #).existsl' : ({a:i} neg (A a) -> #)
-> (neg (exists A) -> #).
```

```%%% Cut Elimination in Classical Sequent Calculusce' : @ -> # -> type.ce_cut'  : ce' (cut^ D E) F
<- ({p:pos A} ce' (D p) (D' p))
<- ({n:neg A} ce' (E n) (E' n))
<- ca' A D' E' F.ce_axiom': ce' (axiom^ N P) (axiom' N P).ce_andr' : ce' (andr^ D1 D2 P) (andr' D1' D2' P)
<- ({p1} ce' (D1 p1) (D1' p1))
<- ({p2} ce' (D2 p2) (D2' p2)).ce_andl1': ce' (andl1^ N1 N) (andl1' N1' N)
<- ({n1} ce' (N1 n1) (N1' n1)).ce_andl2': ce' (andl2^ N2 N) (andl2' N2' N)
<- ({n2} ce' (N2 n2) (N2' n2)).ce_impr' : ce' (impr^ D1 P) (impr' D1' P)
<- ({n1}{p2} ce' (D1 n1 p2) (D1' n1 p2)).ce_impl' : ce' (impl^ D1 D2 N) (impl' D1' D2' N)
<- ({p1} ce' (D1 p1) (D1' p1))
<- ({n2} ce' (D2 n2) (D2' n2)).ce_orr1' : ce' (orr1^ D1 P) (orr1' D1' P)
<- ({p1} ce' (D1 p1) (D1' p1)).ce_orr2' : ce' (orr2^ D2 P) (orr2' D2' P)
<- ({p2} ce' (D2 p2) (D2' p2)).ce_orl'  : ce' (orl^ D1 D2 N) (orl' D1' D2' N)
<- ({n1} ce' (D1 n1) (D1' n1))
<- ({n2} ce' (D2 n2) (D2' n2)).ce_notr' : ce' (notr^ D1 P) (notr' D1' P)
<- ({n1} ce' (D1 n1) (D1' n1)).ce_norl' : ce' (notl^ D1 N) (notl' D1' N)
<- ({p1} ce' (D1 p1) (D1' p1)).ce_truer': ce' (truer^ P) (truer' P).ce_falsel': ce' (falsel^ N) (falsel' N).ce_forallr': ce' (forallr^ D1 P) (forallr' D1' P)
<- ({a:i} {p1:pos (A1 a)} ce' (D1 a p1) (D1' a p1)).ce_foralll': ce' (foralll^ T D1 N) (foralll' T D1' N)
<- ({n1} ce' (D1 n1) (D1' n1)).ce_existsr': ce' (existsr^ T D1 P) (existsr' T D1' P)
<- ({p1} ce' (D1 p1) (D1' p1)).ce_existsl': ce' (existsl^ D1 N) (existsl' D1' N)
<- ({a:i} {n1:neg (A1 a)} ce' (D1 a n1) (D1' a n1)).```

What good is your "logic" if it cannot be used to help people in need?

```dog :	i.
nose :	i.
wet :	nose -> dog -> type.dog_wet: D -> wet nose D.
rover:   dog.?- dog_wet rover
[Quadratic Search Algorithm Employed, initial neural variance 1.06%]
Searching type of dog..... found [dog : i ]
[neural variance 13.24%]
Searching type of wet........ found type more general than specified [wet : water -> OB -> type]
[neural variance 54.21%]
Searching type of rover.......................[neural variance 74.1%].................[WARNING neural variance 88.2%]..........foundnode 75:10.1-10.7 Error: operator and operand don't agree (tycon mismatch)
operator domain: rover : dog
operand:         rover : automobile
in expression:
dog_wet rover[translating].........[assigning persona]........[DONE!]
[time: 123:05.32]
```

A rover is a car dude, not a dog.

Heh. You said beaver. Heh heh.

[Hall of Fame]