Up: Corpus of Examples
Previous: Abstractions, Approximations, and Meta-Rules
Next: Rings
Formalism:
box(R : region) -- Predicate.
inside(R : region) : point-set -- Function.
cavity(R1,R2 : region) -- Predicate
Definitions:
inside(R) = closure(complement(R) -- outside(R))
box(R) < = > inside(R) != empty.
cavity(RC,R) <=> thickly_connected_component(RC,inside(R)).
Characteristics: Topology.
Formalism:
box(R2) ^ P(R1 : region, inside(R2)) =>
P(R2,outside(R1)) ^ P(outside(R2), outside(R1)).
Characteristics: Topology
Formalism:
box(RB1) ^ box(RB2) ^ P(R : region,inside(RB1)) ^ P(R,inside(RB2))
^ rcc_DS(RB1,RB2) =>
[PP(RB1,inside(RB2)) V PP(RB2,inside(RB2))]
Characteristics: Topology.
Formalism:
box(R1) ^ box(R2) ^ P(R1,inside(R2)) =>
PP(inside(R1),inside(R2)).
Characteristics: Topology.
Formalism:
box(R2) ^ P(R1 : region,outside(R2))
=>
PP(R2,outside(R1)) ^ PP(inside(R2),outside(R1)).
Declaration:
thin_box_pt(P : point, R : region) -- Predicate.
thick_box(R : region) -- Predicate.
Formalism:
thin_box_pt(P,R) < = > box(R) ^ P in outside(R) intersect inside(R).
thick_box(R) < = > box(R) ^ not exists(P) thin_box_pt(P,R).
Characteristics: Topology.
Formalism:
thick_box(R) < = > box(R) ^ DC(outside(R),inside(R))
Characteristics: Topology.
Formalism:
rcc_NTTP(R1,R2 : region) => thick_box(R1--R2)
Characteristics: Topology.
Formalism:
forall(R1: region) exists (R2) blob(R2) ^ thick_box(R1 union R2).
Characteristics: Topology.
Formalism:
blob(R1) ^ blob(R2) ^ rcc_EC(R1,R2)
^ SU = boundary(R1) intersect boundary(R2) ^ SU=SU1--SU2 ^
surface_NTPP(SU2,SU1)
=>
box(R1 union R2).
Characteristics: Topology.
Formalism:
box(RB) ^ rcc_DS(R : region,RB) =>
P(R,outside(RB)) V P(R,inside(RB))
Characteristics: Topology.
Formalism:
forall(P1, P2 : point; R : region)
~(P1 in R) ^ ~(P2 in R) ^
[~exists(PS1 : point-set) connected(PS1) ^ in(P1,PS1) ^ in(P2,PS1) ^
DC(PS1,interior(R))] =>
thick_box(R) ^
exists (RC1,RC2)
[RC1 = outside(R) V cavity(RC1,R)] ^
[RC2 = outside(R) V cavity(RC2,R)] ^
RC1 != RC2 ^ in(P1,RC1) ^ in(P2,RC2)
forall(P1, P2 : point; R : region)
~(P1 in R) ^ ~(P2 in R) ^
[~exists(R1 :region) P1 in R1 ^ P2 in R1 ^ rcc_DS(R1,R)] =>
box(R) ^
exists (RC1,RC2)
[RC1 = outside(R) V cavity(RC1,R)] ^
[RC2 = outside(R) V cavity(RC2,R)] ^
RC1 != RC2 ^ in(P1,RC1) ^ in(P2,RC2)
Characteristics: Topology.
Formalism:
box(RB) ^ P(RB,RC) ^ ~P(inside(RB),RC) =>
box(RC) ^ P(inside(RB)--RC, inside(RC)).
Characteristics: Geometry.
Formalism:
box(RA) ^ box(RB) ^ fits_in(RA,inside(RB)) => ~fits_in(RB,inside(RA)).
Characteristics: Geometry.
Formalism:
fits_in(RA,inside(RB)) ^ fits_in(RB,inside(RC)) => fits_in(RA,inside(RC))
Characteristics: Kinematics
Formalism:
box(OB) ^ kinematic(H) ^ S in H ^ S1 in H =>
[holds(S,P*(O1,inside+(OB))) =>
holds(S1,P*(O1,inside+(OB)))] ^
[holds(S,P*(O1,outside+(OB))) =>
holds(S1,P*(O1,outside+(OB)))].
Characteristics: Topology.
Formalism: box(OB) ^ occurs(H,goes_through(OB,OH,OU1,OSU2)) => exists(H1) subhistory(H1,H) ^ occurs(H1,goes_through(inside*(OB),OH,OSU1,OSU2)).
Declaration:
outer_outlet(SU : surface; RH, RC : region) -- Predicate.
inner_outlet(SU : surface; RH, RC : region) -- Predicate.
Formalism
outer_outlet(SU,RH,RC) < = >
outlet(SU,RH,RC) ^ P(SU,outside(RC))
inner_outlet(SU,RH,RC) < = >
outlet(SU,RH,RC) ^ P(SU,inside(RC))
Declaration: g_box_with_holes(RB : region; RHS : set[region]; RC : region) -- Predicate.
Formalism:
g_box_with_holes(RB,RHS,RC) < = >
holes(PHS,RB,RC) ^ box(RC) ^ P(RC,convex_hull(RB)) ^
forall(RH in RHS)
exist(SU1,SU2 : surface)
inner_outlet(SU1,RH,RC) ^ outer_outlet(SU2,RH,RC)
Declaration: box_with_holes(OB: object; PHS : set[pseudo-object]; PC : pseudo-object) -- Predicate
Formalism:
box_with_holes(OB,PHS,PC) < = >
g_box_with_holes(OB,PHS,PC) ^ source(PC) = OB ^ forall(PH in PHS)
source(PH) = OB.
Characteristics: Kinematics
Formalism:
forall(O1, OB : object; PHS : set[pseudo-object]; PC : pseudo-object;
S1,S2 : situation ; H : history);
[box_with_holes(OB,PHS,PC) ^ S1 in H ^ S2 in H ^ kinematic(H) ^
holds(S1,P*(O1,inside+(PC))) ^
holds(S2,P*(O1,outside+(PC))) =>
exists(PH in PHS,PSUI,PSUO,H1) source(PSUI) = source(PSUO) = OB ^
inner_outlet(PSUI,PH,PC) ^ outer_outlet(PSUO,PH,PC) ^
subhistory(H1,H) ^
[ time(S1) < time(S2) => occurs(H1,goes_through(O1,PH,PSUI,PSUO))] ^
[ time(S2) < time(S1) => occurs(H1,goes_through(O1,PH,PSUO,PSUI))].
Corollary: It follows, therefore that, if O goes from inside OB to outside OB, then it fits through some hole in OB. If O does not fit through any hole in OB, then it cannot go from the inside to the outside, or vice versa. (We include this here separately, because it was easier to explain in the conference paper than the more general fact Box.F16.)
Characteristics: Kinematics.
Formalism:
[box_with_holes(OB,PHS,PC) ^
holds(S1,PP*(O1 : object; inside+(PC)) ^
holds(S2,PP*(O1 : object; outside+(PC)) ^
kinematic(H) ^ S1 in H ^ S2 in H] => \\
exists(PH in PHS,PSO,PSI) inner_outlet(PSI,PH,PC) ^
outer_outlet(PSI,PH,PC) ^
fits_through(O,PH,PSI,PSO)
Formalism:
can_exit(O,OB,POC,S) < = >
exists(POHS) box_with_holes(OB,POHS,POC) ^
exists(H) kinematic(H) ^ S = start(H) ^
holds(S,P*(O,inside+(POC)))
holds(end(H),P*(O,outside+(PB)))
Characteristics: Kinematics.
Formalism:
box_with_holes(OB,POHS,POC) ^ can_exit(O,OB,POC,S) =>
exists(POH in POHS, POSUI, POSUO)
inner_outlet(POSUI,POH,POC) ^
outer_outlet(POSUO,POH,POC) ^ source(POSUI) = source(POSUO) = OB ^
fits_through(O,POH,POSUI,POSUO).
Characteristics: Kinematics.
Formalism:
exists(O,OB,PC,PHS,PH,POSUI,POSUO)
box_with_holes(OB,PHS,PC) ^ PH in PHS ^
inner_outlet(POSUI,POH,POC) ^
outer_outlet(POSUO,POH,POC) ^
source(POSUI) = source(POSUO) = POB ^
fits_through(O,POH,POSUI,POSUO) ^
~exists(S) can_exit(O,OB,PC,S)
Characteristics: Kinematics; collection of objects.
Formalism:
forall(O,OB,O1,OB1 : object; PC, PC : pseudo-object; S,S1 : situation)
can_exit(O,OB,PC,S) ^
subset(objects(S1),objects(S)) ^ subset({O,OB},objects(S1)) ^
forall(O in objects(S1)) place(O,S1) = place(O,S) ^
=>
can_exit(O1,OB1,PC,S1).
Characteristics: Kinematics; collection of objects.
Formalism:
forall(O,OB,O1,OB1 : object; PC, PC : pseudo-object; S,S1 : situation)
can_exit(O,OB,PC,S) ^
objects(S1) = (objects(S) -- {O,OB}) union {O1,OB1} ^
P(place(O1,S1),place(O,S)) ^
P(place(OB1,S1),place(OB,S)) ^
forall(O2 in objects(S) -- {O,OB}) place(O,S1) = place(O,S2) ^
exists(PHS1) box_with_holes(OB1,PHS1,PC)
=>
can_exit(O1,OB1,PC,S1).
Declaration:
g_open_box1(RB,RH,RC : region; SU : surface) -- Predicate.
g_open_box(RB : region; SU : surface) -- Predicate.
g_open_box_out(RB : region; SU : surface) : direction -- Function.
g_open_box_inside(RB : region; SU : surface) : region --- Function.
Formalism:
g_open_box1(RB,RH,RC,SU) < = >
g_box_with_holes(RB,{RH},RC) ^ planar(SU) ^ outer_outlet(SU,RH,RC)
g_open_box(RB,SU) < = >
exists(RH,RC) g_open_box1(RB,RH,RC,SU).
g_open_box_out(RB,SU) = D < = >
exists(RH,RC,P) g_open_box1(RB,RH,RC,SU) ^ P in SU ^ D=out_normal(RC,P).
forall (P : point) P in g_open_box_inside(RB,SU) < = >
P in SU V exists(RH,RC) g_open_box(RB,RH,RC,SU) ^ P in inside(RC).
Declaration:
open_box(OB : object; PSU : pseudo-object[surface]) -- Predicate.
open_box_out(OB : object; PSU : pseudo-object[surface]) :
pseudo-object[direction] --- Function.
open_box_inside(OB : object; PSU : pseudo-object[surface]) :
pseudo-object[region]
Formalism:
open_box(OB,PSU) < = > OB = source(PSU) ^ g_open_box(OB,PSU).
open_box_out(OB,PSU) = PD < = > OB = source(PSU) = source(PD) ^ D = open_box+(OB,PSU).
open_box_inside(OB,PSU) = PI < = > OB = source(PSU) = source(PI) ^ PI = open_box_inside+(OB,PSU).
Characteristics: Geometry.
Formalism:
closed_box(RB1) ^ PT in interior(inside(RB1)) ^ plane(PL) ^ PT in PL =>
exists(RB2) connected_component(RB2,RB1 -- PL) ^ PP(SU,PL) ^ open_box(RB2,SU)
^ PT in SU.
Characteristics: Dynamics, probabilistic.
forall(OB,PSU,O1) open_box(OB,PSU) =>
Prob(forall(S in H) holds(S,O*(O1,open_box_inside(OB,PSU)) | dynamic(H) ^ motionless(OB,H) ^ isolated({O1},{OB},H) ^ holds(start(H),open_box_out(OB,SU) =* up) ^ holds(start(H),still(O1))) > 1 -- small_prob.
Comment: If O1 is required to be convex, then the conclusion can be proven deterministically (Davis, 1988). However, this distinction is presumably not part of a commonsense understanding.
Characteristics: Dynamics, probabilistic tendency.
Formalism:
open_box(OB,PSU) => Prob_Tendency (conclusion: forall(S in H) holds(S,O*(O1,open_box_inside(OB,PSU)). givens: isolated({O1},{OB},H) ^ holds(start(H),open_box_out(OB,PSU) =* up) ^ holds(S,still(O1))) influences: [roughness_motion(O1,H),small], [height(SU) -- height(bottom(open_box_inside(OB,PSU)), big] )
Characteristics: Dynamics.
Formalism:
[open_box(OB,SU) ^ convex(open_box_inside(OB,SU)) ^
SU=projection(open_box_inside(OB,SU),SU) ^
holds(S,PP*(O1,open_box_inside(OB,SU))] =>
exists(D : duration) forall(H : history)
[[duration(H) > D ^ forall(S in H) value(S,open_box_out(OB,SU)) = --up ^
isolated({O1},{OB},H)} =>
holds(end(H), DC*(O1,open_box_inside(OB,SU)))]
Declaration:
box_with_lid(OB,OL : object; PI : pseudo-object[region]) : fluent[boolean]
--- Function.
Formalism:
holds(S,box_with_lid(OB,OL,PI)) < = >
source(PI)=OB ^ holds(S,cavity*(PI, OB union* OL)) ^
~holds(S,cavity*(PI, OB)) ^
~holds(S,cavity*(PI, OL)) ^
Characteristics: Kinematics.
Formalism:
[kinematic(H) ^
holds(start(H), box_with_lid(OB,OL,PI)) ^
holds(start(H), P*(O1,PI)) ^
[forall (S in H) exists(PI1) holds(S,box_with_lid(OB,OL,PI1)) ^
holds(S,rcc_O*(PI1,PI))]] =>
[forall (S in H) exists(PI1) holds(S,box_with_lid(OB,OL,PI1)) ^
holds(S, P*(O1,PI1))].
Characteristics: Dynamics, comparative probability, external force, prediction.
Characteristics: Statics, deterministic, prediction,
Characteristics: Kinematics, deterministic, external force, shape from behavior. Note the unusual use of hypothetical objects
Characteristics: Kinematics, probabilistic, external force, shape from behavior.
Characteristics: Kinematics, deterministic, existence of a scenario.
Characteristics: Kinematic, deterministic, prediction of behavior in one scenario from a related scenario.
Characteristics: Dynamics, deterministic, external force, prediction.
Characteristics: Dynamics, probabilistic, external force, prediction.
Characteristics: Dynamics, deterministic, external force, prediction.
Characteristics: Dynamics, suggestive, external force, planning.
Box with crack
Box with open side
Tray
Drawers, compartments.