yuhuanstudio/wikipedia-omni-zh huggingface dataset:
磅巷

磅巷（Pound Lane）是位于香港香港岛上环的一条古老行人楼梯街，南北走向，最高南至医院道，行人再上可以通往坚道与般咸道2号交接的合一堂、前那打素医院（现称罗便臣道80号）及英华女学校等。磅巷北至山下的荷李活道近水坑口街南，及荷李活道公园。

## 历史

磅巷是香港殖民地时期早期华人聚居的地方，于1894年香港鼠疫后，香港政府为了改善区内的卫生环境，1904年于磅巷兴建了首座提供淋浴设备的香港公厕。

## 名称由来

磅巷的“Pound”并非指重量单位“磅”，而是取自当时由英国人设立的一个动物收容所（英文也是“Pound”），音译了事，便翻译成今天的磅巷一词。

## 兴建扶手电梯风波

2008年，政府建议《兴建上坡地区自动扶梯连接系统的评审制度》，加强斜坡之间的连接。

2013年第3季，政府就磅巷扶手电梯项目咨询公众，计算出人流达10,000人次，亦可减省居民步行约300级楼梯。方案推出后受到民间批评，主要原因是被古物古迹办事处界定属二级历史建筑的医院道4号围墙有可能需要被拆除及重置。路政署表示收到约5000份意见书。到2015年1月推出优化方案，修改部分走线。唯磅巷关注组批评，优化方案未回应夸大使用人数的问题。

## 途经景观

- 医院道
- 律打街
- 普庆坊
- 百姓庙
- 卜公花园
- 东华医院
- 太平山街
- 荷李活道
- 天主教总堂区学校

## 基本资料

- 地点：Hong Kong
- 英文街道名称：Pound Lane
- 图片说明：磅巷以北，山下绿树成荫
- 道路长度：0.2
- 车速限制：0
- 所在地区：香港中西区上环
- 起点：荷李活道
- 终点：医院道
- 通车日期：19世纪
教堂桥

教堂桥（Kapellbrücke，音译“卡佩尔桥”）是位于瑞士琉森（Luzern）的一条木结构廊桥，长204米（670英尺），跨越罗伊斯河（Reuss）两岸，接近琉森湖的出口处。这条廊桥是欧洲现存最古老的木质廊桥，是琉森的地标，也是瑞士的一大旅游景点。因为桥的北岸有一座圣彼德教堂（St. Peters-Kirche），所以该桥得名“教堂桥”。

## 构造和历史

<image>

教堂桥建于1333年，本来是为了琉森的防御需要而建。桥身是棕色的，而桥顶髹上红色。在廊桥的里面有约一百二十幅于十七世纪时所绘关于琉森历史的画。不幸地，教堂桥的大部分于1993年因为有人随地丢烟头导致桥被烧掉了很大一部分，事后很快得以重建，回复原来的样貌。

桥中间有一座140英尺高的八角形水塔（Wasserturm），由砖建成。此水塔原本用作监狱、拷问所、瞭望台及金库。现在每到初夏的时候，木桥外侧就开满了天竺葵。

## 绘画

<image>

琉森的三座人行桥，建于十四世纪的霍夫桥（已毁）、教堂桥和建于十六世纪的斯普洛耶桥都以内部的三角形木板画著称这些壁画，据推测大约是十七世纪由当地天主教画家汉斯·海因里希·魏格曼所绘，画作创作于反宗教改革时期，以宣传天主教会思想为主，画上还有捐资者的纹章。

画家所用的木板长150-181厘米，宽85-95厘米。大部分是云杉木，也有一些 椴树和枫树。教堂桥原有158幅壁画，1993年火灾前尚存147幅，火灾后搜集到47幅的残片，其中30幅进行了复原。

## 基本资料

- 座标：47°N 03°E
- 承载：人行
- 跨越：罗伊斯河
- 国家：瑞士
- 地点：琉森州琉森
- 建筑材料：木
- 长度：204米
- 跨数：27
老猫

《老猫》是倪匡笔下著名科幻小说卫斯理系列之一，讲述继《蓝血人》后另一外星人的悲剧故事。

## 内容简述

张老头是一个行为古怪神秘的老人，因他在家中每天不停的发出敲凿声，及搬家时遗留的动物内脏，引起了卫斯理的关注而进入其屋所调查，而当中卫斯理面对的最大敌人竟然是张老头家中一头凶恶的黑猫！交手过程中连卫斯理亦感棘手，后来出动了一头勇敢无比的猛犬“老布”才得以重创这头妖异的黑猫，然而老布亦身负重伤几乎奄奄一息，过程惊心动魄。然而根据黑猫断了的一截尾巴，竟从上面的组织发现出这是一头千年老猫！而张老头和这头黑猫的真正身份亦是本故事的主轴之谜。

据作者提及，《老猫》在卫斯理系列作品中，是备受注意的前十名。本故事亦曾经被改编成广播剧、电影、漫画。其中猫狗大战的部分描写得十分精采，即使是小说亦构成了丰富的视觉效果。而老猫主要想表达出外星人的另一悲剧，类似蓝血人中的外星人有家归不得的无奈。

## 主要人物

- 卫斯理 - 主角的作家。与警方熟悉的人
- 白素 - 卫斯理的妻子。
- 李同 -第一个留意起张老头的住客
- 王杰美 - 年轻警官
- 张老头 - 身份神秘的老人，小说最后暗示，其可能是老猫的同类。
- 老猫 - 活了超过3千年的外星寄居者
- 老陈 - 爱犬之人，老布的主人
- 老布 - 能跟老猫匹敌的猛犬

## 广播剧

- 香港电台于1972年3月28日以粤语首播《老猫》广播剧，合共8集。
- 播音
- 区聪 饰演 卫斯理
- 龙宝钿 饰演 白素

- 香港电台于1981年11月28日及12月5日以粤语首播《老猫》立体声广播剧，合共2集。
- 编导：李安求
- 播音
- 锺伟明 饰演 卫斯理
- 尹芳玲 饰演 白素
- 林友荣 饰演 老猫
- 陈炳球 饰演 张老头
- 熊良锡 饰演 王杰美
- 黄浩义 饰演 李同
- 重温
- 上集
- 下集

- 香港商业电台以粤语于1988年星期一至五，每日下午三时正播出《老猫》广播剧，合共12集。为商台卫斯理广播剧系列第卅一个故事。
- 监制：金贵
- 改编：唐宁
- 播音
- 朱子聪 饰演 卫斯理
- 钱佩卿 饰演 白素
- 杨广培 饰演 王杰美
- 金贵 饰演 张老头
- 金刚 饰演 老丁(原著为老陈)
- 甄锦华 饰演 李同
- 吴忠泰 饰演 警员
- 李锦 饰演 卫斯理朋友
- 陈森 饰演 粗鲁男子
- 陈森 饰演 彭老板(古董店老板)
- 甄锦华 饰演 陈三万(暴发户,原著为陶翁)
- 朱雪梅 饰演 阿彩(仆人)
- 陈慕贤 饰演 陈太太(原创角色)
- 陈永信 饰演 途人
- 吴忠泰 饰演 途人
- 甄锦华 饰演 兽医
- 陈永信 饰演 化验所所长
- 甄锦华 饰演 邮差

- 大陆广州电台于2004年起以粤语首播卫斯理广播剧，由主播讲出《老猫》故事。
- 主播:向安神，少爷明
- 合共17集

## 电影

- 老猫（The Cat），1992年的香港电影
- 导演: 蓝乃才
- 演员表
- 李子雄 饰演 卫斯理
- 伍咏薇 饰演 白素
- 叶蕴仪 饰演 少女
- 刘兆铭 饰演 依洛
- 刘锡贤 饰演 李同
- 特别客串
- 倪匡 饰演 老陈
- 电影预告
- 特摄场面(猫狗大战)

## 漫画

- 新加坡漫画家黄展鸣于1998年8月7日发表了卫斯理《老猫》漫画
- 出版社：台湾时报文化
- 封面: http://addons.books.com.tw/G/8/0010070598.jpg

## 基本资料

- 图像说明：老猫封面
- 作者：卫斯理
- 出版地点：香港
- 语言：中文
- 系列：卫斯理系列
- 类型惊悚：流行文学
- 出版机构：明窗出版社
- 页数：244
- ISBN：9628917579
- 杜威十进分类法：800
- 前作：狐变、聚宝盆
- 续作：天外金球
矩阵正态分布

矩阵常态分配（matrix normal distribution）是一种几率分布，属于常态分配的之一。

几率密度函数相对于随机矩阵（random matrix） X (n × p) 表达如下的矩阵常态分配方式

$$p(\mathbf{X}|\mathbf{M}, {\boldsymbol \Omega}, {\boldsymbol \Sigma}) =(2\pi)^{-np/2} |{\boldsymbol \Omega}|^{-p/2} |{\boldsymbol \Sigma}|^{-n/2} \exp\left( -\frac{1}{2} \mbox{tr}\left[ {\boldsymbol \Omega}^{-1} (\mathbf{X} - \mathbf{M}) {\boldsymbol \Sigma}^{-1} (\mathbf{X} - \mathbf{M})^{T} \right] \right).$$
丹尼斯·欧文

约瑟夫·丹尼士·艾云（Joseph Denis Irwin；1965年10月31日），出生在科克，是前爱尔兰男子职业足球员，司职后卫。他在效力曼联时度过了既漫长却又成功的阶段，亦是在1990年代及2000年代初协助球队赢得许多主要奖杯的最重要球员之一，他因此为人所熟悉。他早期曾效力列斯联和奥咸。

## 早年

艾云成长于科克并就读于高兰斯迪学校。当他还是学童时，他在盖尔式足球和板棍球的表现已胜过他人，他不止一次在克罗克公园球场踼盖尔式足球，其中有一次他就负责防守未来的爱尔兰队友尼尔·昆尼。

## 球会

1983年，艾云在列斯联展开其足球生涯，并在乙组联赛上阵72场赛事，其后在1986年自由转会至奥咸效力。1990年，他协助奥咸打入联赛杯决赛和足总杯四强，于后者虽然被曼联淘汰，但其表现获得青睐。及后，他以62.5万英镑身价加盟曼联。1990年8月25日在奥脱福球场对考文垂首次代表曼联披甲上阵。

艾云在奥脱福球场的12年中，他总共上阵了296场英超赛事，他效力期间曼联赢得七次英超冠军、三次足总杯冠军（1994年、1996年和1999年）、一次联赛杯冠军和欧洲杯赛冠军杯。加盟曼联之初他担任右闸，于1991/92年球季转任左闸，而他可以出任后卫中的任何位置，并且是一名自由球和十二码专家，他在约35岁时依然压过更年轻的菲腊·尼维利成为球队的正选左闸。

2001年4月22日，艾云获佐治·贝斯选为曼联历来最佳十一人之一，与丹尼士·罗、卜比·查尔顿、大卫·贝克汉姆和彼得·舒米高等齐名。

2002年5月12日，艾云在2001/02球季煞科战于奥脱福球场对查尔顿的赛事中最后一次代表曼联上阵，时任曼联领队亚历斯·费格逊将队长臂章交给他，最终双方0-0打成平手。

2002年7月，艾云自由转会至狼队，无独有偶他的前曼联队友保罗·恩斯亦从米杜士堡加盟这支西米德兰兹郡球会。他在处子球季中分别于对般尼和甘士比的赛事中取得入球。

2003年，狼队升班英超后，艾云在步入奥脱福球场时受到曼联球迷鼓掌欢迎。2003/04球季结束后，狼队降班后，已经38岁的他对外宣布退役。

## 退役之后

自2004年，艾云重返奥脱福球场担任MUTV的主持人。

## 国际赛

艾云曾代表爱尔兰上阵56场赛事及攻入四球，亦曾出战1994年世界杯。2005年10月17日，他声称亚历斯·费格逊将会是下任爱尔兰队领队。时隔一日，他却就此事向亚历斯·费格逊道歉。

## 数据

### 球员

球会｜球季｜联赛｜足总杯｜联赛杯｜欧洲赛｜其他｜总计

上阵｜入球｜上阵｜入球｜上阵｜入球｜上阵｜入球｜上阵｜入球｜上阵｜入球

列斯联｜1983/84｜19｜0

1984/85｜41｜1

1985/86｜12｜0

总计｜72｜1｜3｜0｜5｜0｜2｜0

奥咸｜1986/87｜41｜1

1987/88｜43｜0

1988/89｜41｜2

1989/90｜42｜1｜1｜0

总计｜167｜4｜13｜0｜19｜3｜5｜0

曼联｜1990/91｜34｜0｜1｜0｜1｜0

1991/92｜38｜4｜1｜0

1992/93｜40｜5

1993/94｜42｜2｜1｜0｜1｜0

1994/95｜40｜2｜1｜0

1995/96｜31｜1｜1｜0

1996/97｜31｜1｜3｜0｜8｜0

1997/98｜25｜2｜4｜0｜1｜0｜6｜2｜1｜0

1998/99｜29｜2｜6｜1｜11｜0｜1｜0

1999/00｜25｜3｜13｜0｜4｜0

2000/01｜21｜0｜1｜0｜7｜2｜1｜0

2001/02｜12｜0｜10｜0｜1｜0

总计｜368｜22｜43｜7｜31｜0｜87｜4

狼队｜2002/03｜43｜2｜4｜0｜2｜0

2003/04｜32｜0｜1｜0

总计｜75｜2｜5｜0｜2｜0｜3｜0

总计｜682｜29｜64｜7｜57｜3｜97｜4

### 国际赛入球

- ｜日期｜地点｜对手｜入球｜结果｜性质

1｜1992年4月29日｜爱尔兰，都柏林，兰斯当路体育馆｜美国｜2-0｜4-1｜友赛

2｜1997年10月29日｜爱尔兰，都柏林，兰斯当路体育馆｜比利时｜1–0｜1-1｜1998年世界杯外围赛附加赛

3｜1998年9月5日｜爱尔兰，都柏林，兰斯当路体育馆｜克罗地亚｜1-0｜2-0｜2000年欧洲国家杯外围赛

4｜1999年2月10日｜爱尔兰，都柏林，兰斯当路体育馆｜巴拉圭｜1–0｜2-0｜友赛

## 荣誉

### 球会

曼联

- 英超冠军（7）：1992/93年、1993/94年、1995/96年、1996/97年、1998/99年、1999/00年、2000/01年。
- 足总杯冠军（3）：1994年、1996年、1999年。
- 联赛杯冠军（1）：1992年。
- 社区盾（4）：1990年、1993年、1996年、1997年。
- 欧联冠军（1）：1999年。
- 欧洲杯赛冠军杯冠军（1）：1991年。
- 欧洲超级杯冠军（1）：1991年。
- 洲际杯冠军（1）：1999年。

狼队

- 英甲〈第二级〉附加赛冠军（1）：2003年。

个人

- 英格兰足球超级联赛十年奖项十年最佳阵容：1992/93-2001/02年。
- PFA英超年度最佳阵容：1993/94年、1998/99年。

## 外部链接

- Biography at ManUtd.com
莱斯分布

$v\ge 0\,$ $\sigma\ge 0\,$

$$x\in [0;\infty)$$

$$\frac{x}{\sigma^2}\exp\left(\frac{-(x^2+v^2)} {2\sigma^2}\right)I_0\left(\frac{xv}{\sigma^2}\right)$$

$$\sigma \sqrt{\pi/2}\,\,L_{1/2}(-v^2/2\sigma^2)$$

$$2\sigma^2+v^2-\frac{\pi\sigma^2}{2}L_{1/2}^2\left(\frac{-v^2}{2\sigma^2}\right)$$

在概率论与数理统计领域，莱斯分布（Rice distribution或Rician distribution）是一种连续概率分布，以美国科学家斯蒂芬·莱斯的名字命名，其概率密度函数为：

$$f(x|v,\sigma)=\,$$

$$\frac{x}{\sigma^2}\exp\left(\frac{-(x^2+v^2)} {2\sigma^2}\right)I_0\left(\frac{xv}{\sigma^2}\right)$$

其中$I_0(z)$是修正的第一类零阶贝索函数（Bessel function）。当$v=0$时，莱斯分布退化为瑞利分布。

## 极限情况

For large values of the argument, the Laguerre polynomial becomes (See Abramowitz and Stegun §13.5.1 )

$$\lim_{x\rightarrow -\infty}L_\nu(x)=\frac{|x|^\nu}{\Gamma(1+\nu)}$$

It is seen that as $v$ becomes large or $\sigma$ becomes small the mean becomes $v$ and the variance becomes $\sigma^2$

## 相关条目

- Stephen O. Rice (1907-1986)
- 瑞利分布
- 莱斯衰落
M75 (球状星团)

M75（也称为NGC 6864）是一个位于人马座的球状星团，于1780年被梅香发现，并且在同年被梅西耶发现并登录在他的疑似彗星目录中。

M75与地球的距离大约是67,500 光年，将他在天空中的视大小换算成实际的半径约为67光年。他的类型是高度集中的Ⅰ，意思是他是所有已知的球状星团中，核心密度最高的。M75的绝对星等大约是-8.5等，光度相当于或超过180,000颗太阳。

## 外部链接

- Messier 75 @ SEDS Messier pages

## 基本资料

- 日语原文：梅西耶75
- 历元：J2000
- 分类：I
- 星座：人马座
- 赤经：20
- 赤纬：-21
- 距离：67.5 kly
- 距离：20.7 kpc
- 视星等（V）：+9.18
- 视直径（V）：6′.8
- 半径：67 ly
- 其它名称：M75, NGC 6864, GCl 116
东印度公司书院

东印度公司书院（East India Company College）成立于1805年，于1858年关闭，是附属于英国东印度公司的书院。

书院为16至18岁学生教授一般知识，并提供职业培训。学生均须由东印度公司的董事推荐到公司的海外文官部门，方会被取录。学生通常要上四个学期，每学期为6个月。

## 历史

<image>

书院最初设于赫特福德城堡（Hertford Castle）作为临时校舍，随后于1809年迁至赫特福德附近赫特福德荒原的新校舍，而该校舍现今成为黑利伯里及帝国服务书院）（Haileybury College）。书院校舍由建筑师威廉·威尔金兹（William Wilkins）所设计，威尔金兹随后曾设计伦敦的英国国立美术馆，两者在风格上十分相似。

在1856年，书院的取录方法由以往靠董事推荐，改由以富竞争的入学考试选取学生。到了1857年，印度本土爆发了民族起义，英国政府遂在1858年1月从东印度公司接管印度的行政权，书院亦随之关闭。

## 著名教授

托马斯·罗伯特·马尔萨斯自1805年起在书院任教，并且是英国首位政治经济学教授。至于查尔斯·巴贝奇就曾于1816年在该校寻求教席。詹姆士·麦金托什（James Mackintosh）则自1818年至1824年在书院教授法律和政治。另外，书院更常设有波斯语教授，以教授亚洲语言。

## 著名校友

- 亨利·巴特尔·弗里尔
- 约翰·罗素·科尔文
古坑交流道 (台78线)

古坑交流道位于台湾云林县斗六市与古坑乡交界处，是连结台3线的交流道，指标为台78线39k，于2004年1月12日通车，往西可与国道一号连接，往东可与国道三号连接。

PH｜39｜PH｜斗六

古坑剑湖山世界

## 邻近设施及出口预告

东行主要出口预告｜邻近设施｜西行出口预告

39

斗 六Douliu｜古 坑Gukeng 右 线RIGHT LANE

示意图

39

PH 古 坑Gukeng 斗 六Douliu 右 线RIGHT LANE

东行次要出口预告

剑 湖 山 世 界Jianhushan Fancy World 右 线RIGHT LANE

## 基本资料

- 日语原文：古坑交流道
- 英文名：Gukeng Interchange
- rd_type：EX
- rd_number：78
- 出口数：39
- exit_name：古坑
- 所在地：台湾云林县斗六市古坑乡
- 通往：古坑乡斗六市剑湖山世界
- 车辆类别：单叶型
- 启用日期：2002年2月6日（西出东入）、2004年1月12日（东出西入）
虎尾交流道 (国道1号)

虎尾交流道为台湾国道1号的交流道，位于台湾云林县虎尾镇，指标原为236k，收费方式改为里程计费后调整为235K，衔接县道145乙线，是高铁云林站的联外交流道，于2012年4月21日启用。

NH｜235｜CH｜斗六

虎尾高铁站

## 周边公路系统

- PH
- CH
- CH
- TRYL
- TRYL
- TRYL
- TRYL

## 邻近设施及出口预告

南下出口预告｜邻近设施｜北上出口预告

235

斗 六Douliou｜虎 尾Huwei 右 线RIGHT LANE

示意图

235

CH

虎 尾Huwei｜斗 六Douliou

右 线RIGHT LANE

## 外部链接

- 交通部高速公路局之 国道一号虎尾交流道示意图

## 基本资料

- 日语原文：虎尾交流道
- 英文名：Huwei Interchange
- rd_type：NH
- rd_number：1
- 出口数：235
- exit_name：虎尾
- 域：虎尾交流道南下出口
- 别名：高铁云林交流道
- 所在地：台湾云林县虎尾镇
- connect：CH（斗六联络道）
- 通往：虎尾镇、斗六市、高铁云林站
- 车辆类别：钻石型
- 启用日期：2012年4月21日
东势交流道

东势交流道为台湾台78线的交流道，位于台湾云林县东势乡，指标为8K，往东可与国道一号和国道三号连接。

PH｜8｜CH｜麦寮

东势

## 邻近设施及出口预告

东行出口预告｜邻近设施｜西行出口预告

8

麦 寮Mailiao｜东 势Dongshi 右 线RIGHT LANE

示意图

8

CH

东 势Dongshi｜麦 寮Mailiao

右 线RIGHT LANE

## 外部链接

- 台78线东势交流道示意图 （交通部公路总局）

## 基本资料

- 英文名：Dongshi Interchange
- rd_type：EX
- rd_number：78
- 出口数：8
- exit_name：东势
- 所在地：台湾云林县东势乡
- 通往：东势乡麦寮乡
- 车辆类别：钻石型
- 启用日期：2003年9月3日（西出东入）、2003年12月8日（东出西入）
台西交流道

台西交流道是台61线、台78线及台17线立体交叉的交流道，位于台湾云林县四湖乡、台西乡。台61线指标为233K；台78线指标为0K。于2014年8月31日通车 台西乡交流道 明通车，2014年8月30日，中国时报，沿台78线往东可与国道一号和国道三号连结。

PH｜233｜PH｜古坑

台西

PH｜0｜PH｜口湖

麦寮

PH｜台西

四湖

## 与北门交流道的差异

台西交流道与北门交流道同样都是东西向快速公路和台61线、台17线立体交叉，两者差异如下：

- 台78线主线起点为台61线高架以西约0.1k到台17线为1公里，因此从台61线分出匝道衔接台78主线后再分出匝道下台17线。
- 台84线主线起点为台61线高架以东0K到台17线为0.5公里，从台61线先分出4匝道，南北向2匝道直下平面联络道路衔接台17线，另2匝道采高架跨越台17线无缝衔接台84主线高架桥，平面联络道路（台84线0.5k）与台17线平面交叉后亦可往东衔接台84主线高架桥。
- 台78线与台61线以高架对高架立体交叉，2条快速公路皆设有侧车道，可以穿越台78线与台61线主线高架桥底下并互相联络。
- 台84线与台61线以高架对平面道路立体交叉，快速公路未设有侧车道，但台17线以东之台84线主线设有侧车道直通下营系统交流道。

## 邻近设施及出口预告

台61线出口预告｜邻近设施｜台78线东行往台17线出口预告

233

古 坑Gukeng｜台 西Taixi ⬈

示意图

0

台 西Taixi｜四 湖Sihu ⬈

台78线西行往台17线出口预告

0

四 湖Sihu｜台 西Taixi ⬈

台78线西行往台61线出口预告

口 湖Kouhu ⬆｜0 PH北NORTH 麦 寮Mailiao ⬆

## 外部链接

- 交通部公路局之 台61线、台78线台西交流道示意图

## 基本资料

- 英文名：Taixi Interchange
- rd_type：EX
- rd_type2：EX
- rd_number：61
- rd_number2：78
- 出口数：233
- 出口数：0
- exit_name：台西
- 别称：台西系统交流道
- 所在地：台湾云林县、四湖乡台西乡
- 通往：台西乡四湖乡
- 车辆类别：喇叭型A、简易钻石型
- 启用日期：2006年4月14日（平交匝道）、2014年1月20日（PH立体化）、2014年8月31日（PH立体化）
斗南交流道 (台78线)

斗南交流道位于台湾云林县大埤乡，是连结台1线的交流道，指标为台78线32K，于2003年1月28日通车。此交流道一开始只设计为东出西入匝道，经地方民意代表争取之下，交通部公路总局（今交通部公路局）便增设西出东入匝道，于2013年11月28日完工通车。

PH｜32｜PH｜斗南

大林

## 邻近设施及出口预告

邻近设施｜出口预告

示意图

32

PH

斗 南Dounan｜大 林Dalin

右 线RIGHT LANE

## 基本资料

- 日语原文：斗南交流道
- 英文名：Dounan Interchange
- rd_type：EX
- rd_number：78
- 出口数：32
- exit_name：斗南
- 所在地：台湾云林县大埤乡
- 通往：云林县斗南镇嘉义县大林镇
- 车辆类别：部分苜蓿叶型交流道
- 启用日期：2003年1月28日（东出西入）、2013年11月28日（西出东入）
头屋一交流道

头屋一交流道为台湾台72线的交流道，位于台湾苗栗县头屋乡，指标为10K，在2001年1月通车，可衔接台13线通往国道一号之头屋交流道。

PH｜10｜PH｜头屋

苗栗NH头屋交流道

## 周边公路系统

- NH：头屋交流道
- PH
- PH
- TRML

## 邻近设施及出口预告

东行出口预告｜邻近设施｜西行出口预告

10

头 屋Touwu｜苗 栗Miaoli 右 线RIGHT LANE

示意图

10

PH

苗 栗Miaoli｜头 屋Touwu

右 线RIGHT LANE

## 外部链接

- 交通部公路局之 台72线头屋一交流道示意图

## 基本资料

- 英文名：Touwu First Interchange
- rd_type：EX
- rd_number：72
- 出口数：10
- exit_name：头屋一
- 所在地：台湾苗栗县头屋乡
- 通往：头屋乡苗栗市、NH头屋交流道
- 车辆类别：单点钻石型
- 启用日期：2001年1月
扬克顿县 (南达科他州)

<image>

扬克顿县（Yankton County）是美国南达科他州东南部的一个县，南隔密苏里河与内布拉斯加州相望。面积1,379平方公里。根据美国2000年人口普查，共有人口21,652人。县治扬克顿（Yankton）。

成立于1862年，县名纪念扬克顿族（苏族的一支）。
波旁县 (肯塔基州)

波旁县（Bourbon County）是美国肯塔基州蓝草地区的一个县，面积755平方公里。根据2020年美国人口普查，共有人口20,252人；2023年估计人口有20,134人。县治巴黎（Paris）。该县成立于1785年5月1日，县名纪念法国的波旁王朝。

本县是波本威士忌的诞生地。

## 基本资料

- 县：Bourbon County
- CN_county：波旁县
- 州：肯塔基州
- founded year：1785年
- seat wl：巴黎
- largest city wl：巴黎
- 总计：292
- 陆地：290
- 水域：1.9
- area percentage：0.6
- 人口：2020
- 人口：20252
- pop_est_as_of：2023
- 估计：20134人
- 人口密度：auto
- 时区：Eastern
- 网站：www.bourbonky.com/
- 名称来源：波旁王朝
- ex image cap：波旁县行政中心
- 区：第6选区
苏聪 (作曲家)

苏聪（1957年），生于中国天津，祖籍广东东莞，作曲家，现定居于德国。

1978年到1982年，苏聪就读于中央音乐学院作曲系。1982年入学德国慕尼黑音乐学院作曲系研究生班。1985年毕业后任教于该院。并在奥格斯堡大学音乐系授课，现任巴登州电影学院及斯图加特市音乐高等学院教授。1988年，因为影片《末代皇帝》作曲而获得第60届奥斯卡最佳电影音乐奖。苏聪获得的其他奖项还包括美国广播音乐公司奖、格莱美最佳背景音乐原作专辑、德国埃森克鲁普基金会奖学金等。
波旁县 (堪萨斯州)

波旁县（Bourbon County，简称BB）是美国堪萨斯州东部的一个县，东邻密苏里州。面积1,655平方公里。根据美国2000年人口普查，共有人口15,379人。县治斯科特堡（Fort Scott）。

成立于1855年8月25日。县名来自肯塔基州同名的县。

## 基本资料

- 县：Bourbon County
- county_zh：波旁县
- 成立：1855年8月25日
- 名称来源：肯塔基州波旁县
- 总面积：1,655
- 总计：639
- 陆地：1,650
- 陆地：637
- 水域：4
- 水域：2
- area percentage：0.27%
- census estimate yr：2006
- 人口：14,950
- 密度：9.1
- 密度：23.5
- 时区：Central
- 网站：www.bourboncountyks.org
利贞

利贞（1172年）是大理国皇帝段智兴的第一个年号，共计4年。

年号名称，云南文献皆作“利贞”，唯《桂海虞衡志》作“利正”。

起讫年，方诗铭、李崇智、段玉明、李家瑞、王云、黄德荣作1172年－1175年。

## 年号及改元出处

- 倪辂《南诏野史》：“宋孝宗乾通八年（1172）立，改元利贞，又改元亨时、元嘉、元亨、安定等号。……智兴卒，在位二十九年。”
- 胡蔚《增订南诏野史》：“南宋孝宗壬辰乾道八年（1172）即位。明年（1173），改元利贞。又改元盛德、嘉会、元亨、安定。……宁宗庚申庆元六年（1200），智兴卒，在位二十八年。”
- 王崧《云南备征志》：“宋孝宗乾道八年（1172）立，改元利贞。……丁酉（1177），改元亨时。……辛丑（1181），改元嘉会。乙巳（1185），改元亨利，又改安定。……庚申宋宁宗庆元六年（1200）七月，帝薨，在位二十九年。”
- 诸葛元声《滇史》：“段氏十八世智兴，以宋孝宗乾道八年壬辰（1172）立，改元利贞。……淳熙八年（1181），……是岁，智兴改元嘉会。……智兴在位二十九年。”
- 李京《云南志略》：“子政智立，改元利贞、盛德、嘉会、元亨、安定。在位二十九年。”
- 杨慎《滇载记》：“智兴以宋孝宗乾道八年（1172）立，改元五，曰利贞、盛德、嘉会、元亨、安定。”
- 冯苏《滇考》：“孝宗乾道八年（1172），子智兴嗣，改元利贞、嘉会。……在位二十九年卒。”
- 《白古通记浅述》：“智兴立二十九年。”
- 《文献通考》卷329引《桂海虞衡志》：“乾道癸巳冬。忽有大理人李观音得、董六斤黑、张般若师等率以三字为名，凡二十三人至横山议市马。出一文书，……称利正二年十二月。”

## 纪年对照表

利贞｜元年｜二年｜三年｜四年

公元｜1172年｜1173年｜1174年｜1175年

干支｜壬辰｜癸巳｜甲午｜乙未

## 同期存在的其他政权年号

- 中国
- 乾道（1165年－1173年）：宋－宋孝宗赵昚之年号
- 淳熙（1174年－1189年）：宋－宋孝宗赵昚之年号
- 崇福（1164年－1177年）：西辽－承天后耶律普速完之年号
- 大定（1161年－1189年）：金－金世宗完颜雍之年号
- 乾祐（1170年－1193年）：西夏－夏仁宗李仁孝之年号
- 日本
- 承安（1171年－1175年）：高仓天皇之年号
- 安元（1175年－1177年）：高仓天皇之年号
- 越南
- 政隆宝应（1163年－1174年）：李朝－李天祚之年号
- 天感至宝（1174年－1175年）：李天祚之年号
菊芋

菊芋（Helianthus tuberosus，Jerusalem artichoke）也称洋姜、鬼子姜、姜不辣、块茎向日葵，是一种菊科向日葵属宿根性草本植物。原产北美洲中部，十七世纪传入欧洲，后传入中国。

## 特征

秋季开花，长有黄色的小盘花，但结籽率低；长江以南可形成种子。洋姜外型一般近似单指生姜，有些品种也偏圆形，看起来像小芋头。

## 食用

其地下块茎富含淀粉、菊糖，可以食用，也可盐渍，或作制取淀粉和酒精原料。地上茎也可加工作饲料。洋姜的薄皮并没有什么特殊味道，也不影响口感，所以在烹饪它时也不一定要去皮。在做菜时，最好把已经去皮或切好的洋姜放在一碗冷水里，滴上几滴柠檬汁或醋，这样可以让它不容易变色。洋姜可以生吃。生洋姜口感新鲜清脆，可以切成片，和口感类似的其他蔬菜水果一起做成沙拉。也可以用做马铃薯的方法来烹饪洋姜。菊芋被联合国粮农组织列为“21世纪人畜共用作物”。

## 种植

生产上一般用块茎繁殖。洋姜为多年生植物，也不太容易受虫害，不用太费心就能重复收获。春季三四月就可以开始种植，等待几个月的成长，收获的季节通常从十一月开始，直到次年三月。在市场上买到洋姜时，它的皮上通常都还带着土。表层的泥土其实能起到保护作用，让洋姜保存的时间更长。因为洋姜的皮很薄，最好不要在用前就着急洗掉泥土，或是去皮和切开。洋姜在阴凉处放置可以保存大概10天左右，但如果已经清洗处理过了的话，即使在冰箱冷藏室也只能保存两三天时间。

## 图片

<image>

- 未开花

<image>

- 花

<image>

- 花和叶子

<image>

- 洗块茎

## 外部链接

- 菊芋 《中国植物志》
- 块茎图片
- 菊芋 Juyu 药用植物图像数据库 (香港浸会大学中医药学院)

## 基本资料

- 学名：Helianthus tuberosus
- 状态：LC
- status_system：iucn3.1
- 命名者：L.
劳伦斯县 (南达科他州)

劳伦斯郡（Lawrence County）是美国南达科他州西部的一个县，西邻怀俄明州。面积2,073平方公里。根据美国2000年人口普查，共有人口21,802人。县治戴德伍德。

成立于1877年，县名纪念该县首任财务长约翰·劳伦斯。

## 基本资料

- 县：Lawrence County
- CN_county：劳伦斯县
- 州：南达科他州
- 成立时间：1月11日
- founded year：1875年
- seat wl：戴德伍德
- largest city wl：斯皮尔菲什
- 总计：800
- 陆地：800
- 水域：0.3
- area percentage：0.03
- 人口统计时间：2020
- 人口：25768
- 密度：auto
- 时区：Mountain
- 网站：http://www.lawrence.sd.us/
- 名称来源：John Lawrence
- ex image cap：县法院
- 区：单一国会选区
布尤特县 (南达科他州)

布尤特县（Butte County）是美国南达科他州西部的一个县，西邻怀俄明州和蒙大拿州，面积5,870平方公里。根据2020年美国人口普查，共有人口10,243人。县治贝尔富什（Belle Fourche）。该县成立于1883年3月2日，县名来自当地的地理特征孤丘。

美国（包括阿拉斯加州和夏威夷州）的地理中心位于县治以北32公里处。

## 基本资料

- 县：Butte County
- CN_county：布尤特县
- 州：南达科他州
- 成立：1883年3月2日
- seat wl：贝尔富什
- largest city wl：贝尔富什
- 总计：2266
- 陆地：2250
- 水域：16
- area percentage：0.7
- 人口：2020
- 人口：10243
- pop_est_as_of：2024
- 估计：10,891人
- density_sq_mi：4.55
- 时区：Mountain
- 网站：butte.sdcounties.org
- 名称来源：境内地形
- ex image cap：布尤特县政府
- 区：单一选区
掘断龙

掘断龙是香港一个已经没有使用的本土地名，根据文献记载，可指以下两个地方。

一个名为掘断龙的地方位于上环街市附近。1851年，崇真会的韩山明牧师在该地向浸信会租赁了两间破屋，设立客家话礼拜堂，举行主日崇拜及一般聚会。

另一个则位于香港岛湾仔鹅颈山与湾仔岭之间的凹陷处，约为现时的活道。自1843年起此处由喼道贯穿，于20世纪初掘断龙定义更沿着皇后大道东向西伸延至石水渠街一带。
哈姆林县 (南达科他州)

哈姆林县（Hamlin County）是美国南达科他州东部的一个县，面积1,393平方公里。根据2020年美国人口普查，共有人口6,164人。县治海提（Hayti）。该县成立于1872年，县政府成立于1878年；县名纪念亚伯拉罕·林肯的第一任副总统汉尼巴尔·哈姆林（Hannibal Hamlin）。

## 基本资料

- 县：Hamlin County
- CN_county：哈姆林县
- 州：南达科他州
- founded year：1873年
- seat wl：海提
- largest city wl：埃斯特莱恩
- 总计：538
- 陆地：507
- 水域：31
- area percentage：5.7
- 人口：2020
- 人口：6164
- pop_est_as_of：2023
- 估计：6451人
- 人口密度：auto
- 时区：Central
- 名称来源：汉尼巴尔·哈姆林
- ex image cap：哈姆林郡政府摄于1974年
- 区：单一选区
元朗剧院

元朗剧院（Yuen Long Theatre）是香港的一个剧场，位于新界元朗区元朗体育路9号，于2000年5月启用。此为元朗区的居民提供一个标准的大型表演及文娱活动场地。元朗剧院建成之前，区内的大型表演都在聿修堂中进行。元朗剧院附近亦有一名为元朗大会堂的建筑，其虽然名为“大会堂”，但不是公共表演场地，而是元朗区的私人志愿社会机构的所在地。

元朗剧院位于元朗新市镇西南角，毗邻元朗公园、元朗大球场和元朗公众泳池；大堂内特设竹林庭园，带出宁静雅致的文化气息。

## 设施

剧院设有一个923个座位的演艺厅、180平方米的舞蹈室、192平方米的排演室、117平方米的演讲室和120平方米的大堂展览场地。

## 基本资料

- 日语原文：元朗剧院、Yuen Long Theatre
- 地址：香港新界元朗区元朗体育路9号
- 启用：2000年5月
元亨 (大理)

元亨（1185年）是大理国皇帝段智兴的第四个年号，共计11年。1195年四月以后改元定安。

年号名称，云南文献大多作“元亨”，唯王崧《云南备征志》及《道光云南志钞》分别作“亨利”及“元贞”。李崇智谓当是“元亨”之误。根据云姚安县《兴宝寺德化铭》及1959年7月在云南大理县弘圭山发现的《大理国彦贲赵兴明为亡母造尊胜墓幢》可知，年号是“元亨”。

起讫年，方诗铭、李崇智、李家瑞作1185-？段玉明、王云、黄德荣作1185年－1195年。

## 年号及改元出处

- 倪辂《南诏野史》：“宋孝宗乾通八年（1172）立，改元利贞，又改元亨时、元嘉、元亨、安定等号。……智兴卒，在位二十九年。”
- 胡蔚《增订南诏野史》：“南宋孝宗壬辰乾道八年（1172）即位。明年（1173），改元利贞。又改元盛德、嘉会、元亨、安定。……宁宗庚申庆元六年（1200），智兴卒，在位二十八年。”
- 王崧《云南备征志》：“宋孝宗乾道八年（1172）立，改元利贞。……丁酉（1177），改元亨时。……辛丑（1181），改元嘉会。乙巳（1185），改元亨利，又改安定。……庚申宋宁宗庆元六年（1200）七月，帝薨，在位二十九年。”
- 诸葛元声《滇史》：“段氏十八世智兴，以宋孝宗乾道八年壬辰（1172）立，改元利贞。……淳熙八年（1181），……是岁，智兴改元嘉会。……智兴在位二十九年。”
- 李京《云南志略》：“子政智立，改元利贞、盛德、嘉会、元亨、安定。在位二十九年。”
- 杨慎《滇载记》：“智兴以宋孝宗乾道八年（1172）立，改元五，曰利贞、盛德、嘉会、元亨、安定。”
- 冯苏《滇考》：“孝宗乾道八年（1172），子智兴嗣，改元利贞、嘉会。……在位二十九年卒。”
- 《白古通记浅述》：“智兴立二十九年。”
- 《兴宝寺德化铭》：“元亨二年岁在丙午七月十五日。”
- 《大理国彦贲赵兴明为亡母造尊胜墓幢》：“元亨十一年岁遇乙卯三月六日辛卯迁化四月十日乙丑设。”

## 纪年对照表

元亨｜元年｜二年｜三年｜四年｜五年｜六年｜七年｜八年｜九年｜十年

公元｜1185年｜1186年｜1187年｜1188年｜1189年｜1190年｜1191年｜1192年｜1193年｜1194年

干支｜乙巳｜丙午｜丁未｜戊申｜己酉｜庚戌｜辛亥｜壬子｜癸丑｜甲寅

元亨｜十一年

公元｜1195年

干支｜乙卯

## 同期存在的其他政权年号

- 中国
- 淳熙（1174年－1189年）：宋－宋孝宗赵昚之年号
- 绍熙（1190年－1194年）：宋－宋光宗赵惇之年号
- 庆元（1195年－1200年）：宋－宋宁宗赵扩之年号
- 天禧（1178年－1211年）：西辽－末主耶律直鲁古之年号
- 大定（1161年－1189年）：金－金世宗完颜雍之年号
- 明昌（1190年－1196年）：金－金章宗完颜璟之年号
- 乾祐（1170年－1193年）：西夏－夏仁宗李仁孝之年号
- 天庆（1194年－1206年）：西夏－夏桓宗李纯祐之年号
- 日本
- 元历（1184年－1185年）：后鸟羽天皇与源氏之年号
- 文治（1185年－1190年）：后鸟羽天皇与源氏之年号
- 建久（1190年－1199年）：后鸟羽天皇、土御门天皇与源氏之年号
- 越南
- 贞符（1176年－1186年）：李朝－李龙翰之年号
- 天资嘉瑞（1186年－1202年）：李朝－李龙翰之年号
定安 (年号)

定安（1195年）是大理国皇帝段智兴的第五个年号，共计6年。

云南文献均作“安定”，根据1984年云南大理挖色镇高兴寺遗址出土碑刻《大理国高与兰若碑》可知，年号是“定安”，云南文献皆倒误。

王崧《云南备征志》云“庚申宋宁宗庆元六年（1200年）七月，帝（段智兴）薨”，段兴廉“八月即位，改元凤历”，则定安终于1200年七月。

起讫年，方诗铭、李崇智、李家瑞作？－1200年，段玉明作1195年－1199年，王云、黄德荣作1195年－1200年。

## 年号及改元出处

- 倪辂《南诏野史》：“宋孝宗乾通八年（1172）立，改元利贞，又改元亨时、元嘉、元亨、安定等号。……智兴卒，在位二十九年。”
- 胡蔚《增订南诏野史》：“南宋孝宗壬辰乾道八年（1172）即位。明年（1173），改元利贞。又改元盛德、嘉会、元亨、安定。……宁宗庚申庆元六年（1200），智兴卒，在位二十八年。”
- 王崧《云南备征志》：“宋孝宗乾道八年（1172）立，改元利贞。……丁酉（1177），改元亨时。……辛丑（1181），改元嘉会。乙巳（1185），改元亨利，又改安定。……庚申宋宁宗庆元六年（1200）七月，帝薨，在位二十九年。”
- 诸葛元声《滇史》：“段氏十八世智兴，以宋孝宗乾道八年壬辰（1172）立，改元利贞。……淳熙八年（1181），……是岁，智兴改元嘉会。……智兴在位二十九年。”
- 李京《云南志略》：“子政智立，改元利贞、盛德、嘉会、元亨、安定。在位二十九年。”
- 杨慎《滇载记》：“智兴以宋孝宗乾道八年（1172）立，改元五，曰利贞、盛德、嘉会、元亨、安定。”
- 冯苏《滇考》：“孝宗乾道八年（1172），子智兴嗣，改元利贞、嘉会。……在位二十九年卒。”
- 《白古通记浅述》：“智兴立二十九年。”
- 《大理国释氏戒净建绘高兴兰若篆烛碑并序》：“定安四年皇帝无大朝戊午岁正月六日。”

## 纪年对照表

定安｜元年｜二年｜三年｜四年｜五年｜六年

公元｜1195年｜1196年｜1197年｜1198年｜1199年｜1200年

干支｜乙卯｜丙辰｜丁巳｜戊午｜己未｜庚申

## 同期存在的其他政权年号

- 中国
- 绍熙（1190年－1194年）：宋－宋光宗赵惇之年号
- 庆元（1195年－1200年）：宋－宋宁宗赵扩之年号
- 天禧（1178年－1211年）：西辽－辽末主耶律直鲁古之年号
- 明昌（1190年－1196年）：金－金章宗完颜璟之年号
- 承安（1196年－1200年）：金－金章宗完颜璟之年号
- 天庆（1194年－1206年）：西夏－夏桓宗李纯祐之年号
- 日本
- 建久（1190年－1199年）：后鸟羽天皇、土御门天皇与源氏之年号
- 正治（1199年－1201年）：土御门天皇与源氏之年号
- 越南
- 天资嘉瑞（1186年－1202年）：李朝－李龙翰之年号
派克县 (亚拉巴马州)

<image>

派克县（Pike County）是位于美国亚拉巴马州东南部的一个县，县治特洛伊。根据美国人口调查局2000年统计，共有人口29,605，其中白人占60.77%、非裔美国人占36.6%。
高分辨率影音网络协会

<image>

高分辨率影音网络协会（High Definition Audio-Video Network Alliance）是一个由媒体业界领导公司组成的组织，用以制定稳固的高清影音网络的工业设计指标。该协会于2005年10月由Charter Communications、JVC、美国松下数位电子公司、美国国家广播环球公司、三星及昇阳共同创立。除创办成员的公司外安谋、飞思卡尔半导体与Pulse~LINK被列为HANA的赞助成员。其在2009年解散，由IEEE 1394协会承接其知识产权。

## 慨观

HANA的任务为制定工业设计指标，利用现存的技术与规格帮助消费者：

- 同时观赏、暂停与录制5个或更多高清频道而不减低服务品质
- 只使用一个机顶盒即可于家中任何地方观赏、暂停与录制高清内容
- 自个人电脑共享个人内容到AV装置时保持受保謢内容的安全
- 每个房间只需一个遥控器即可控制所有AV装置与存取内容
- 只需使用一条IEEE 1394火线即可增加任何装置到家用网络

HANA兼容产品将会包括HDTV、下一代DVD播放器、数位影像录影机、机顶盒与家庭影院。首个商品化的产品预期会在2007年的CES上出现。该协会计划以通过兼容测试及HANA组织开发者的协商来增加不同制造商产品之间的相容性。
兰道夫县 (亚拉巴马州)

<image>

兰道夫县（Randolph County）是位于美国亚拉巴马州东部的一个县，县治韦道伊。根据美国人口调查局2000年统计，共有人口22,380，其中白人占76.38%、非裔美国人占22.24%。
自动化定理证明

<image>

自动化定理证明（Automated theorem proving，简称ATP）是自动推理（AR）体系中发展最成熟的子领域，其目的是使用电子计算机程序来进行数学定理的证明。对于不同的公理系统，自动定理证明器能够推论出一个定理在此系统下是正确的、不可证明的还是错误的。

## 逻辑基础

形式化逻辑的根源可追溯至亚里士多德，但现代逻辑和形式化数学的发展主要在19世纪末至20世纪初。戈特洛布·弗雷格的《概念文字》（1879年）引入了完备的命题逻辑和本质上是现代谓词逻辑的系统。伯特兰·罗素和阿尔弗雷德·诺思·怀特黑德在1910–1913年出版的《数学原理》中延续了这一方向，试图从形式逻辑的公理和推理规则推导出所有数学真理，从原则上开启了自动化的可能。

1920年，托拉尔夫·斯科伦简化了利奥波德·勒文海姆先前的结果，提出了勒文海姆–斯科伦定理；1930年，雅克·埃尔布朗的工作引入了埃尔布朗宇宙和埃尔布朗解释的概念，将一阶公式的（不）可满足性归约为（可能无限的）命题可满足性问题。1929年，莫伊塞斯·普雷斯布格证明，带有加法和等式的自然数一阶理论（今称普雷斯布格算术）是可判定的，并给出了判定算法。

然而，库尔特·哥德尔在1931年发表的《论《数学原理》及相关体系的形式不可判定命题》表明，在任何足够强的公理化系统中，都存在真而不可证的命题（哥德尔不完备定理）。这一主题在1930年代由阿隆佐·邱奇和艾伦·图灵进一步发展，他们分别给出了可计算性的等价定义，并提供了不可判定问题的具体例证。

## 早期实现

1954年，马丁·戴维斯在普林斯顿高等研究院的JOHNNIAC真空管计算机上实现了普雷斯布格的算法。据戴维斯所说，其“最大的成功是证明了两个偶数之和为偶数”。更为雄心勃勃的是1956年的逻辑理论家程序，由艾伦·纽厄尔、赫伯特·西蒙和克利夫·肖开发，用于证明《数学原理》中的命题逻辑定理。该程序使用启发式引导，成功证明了《数学原理》第二章52条定理中的38条。

逻辑理论家的启发式方法试图模拟人类数学家，但无法保证对所有有效定理都能找到证明。与此相对，更系统的算法（基于埃尔布朗和斯科伦的结果）在一阶逻辑中至少从理论上实现了完备性。吉尔摩的程序通过将公式转化为析取范式来检查不可满足性。

## 可判定性与局限

公式有效性的判定问题因底层逻辑的不同而从平凡到不可解不等。命题逻辑是可判定的，但属于co-NP完全问题，一般认为仅存在指数时间算法。对于一阶谓词演算，哥德尔完备性定理指出有效公式恰恰是可证明的公式，因此有效公式是可计算枚举的：在无限资源下，任何有效公式最终都能被证明。然而，_无效_公式（不被理论蕴涵的公式）并非总能被识别。

上述结论适用于一阶理论（如皮亚诺算术）。然而，对于一阶理论描述的特定模型，某些语句可能为真但在所用理论中不可判定。哥德尔不完备定理表明，任何其公理对自然数为真的一致理论都无法证明所有对自然数为真的一阶语句。

## 应用

自动定理证明的商业应用主要集中在集成电路设计与验证领域。自奔腾FDIV缺陷之后，现代微处理器的复杂浮点运算单元在设计时受到了额外的审查。AMD、英特尔等公司使用自动定理证明来验证除法及其他运算的正确实现。其他用途包括程序综合（构造满足形式化规格的程序）以及与证明助手（如Isabelle/HOL）的集成。定理证明器也被应用于自然语言处理和形式语义学领域，用于分析话语表示。

## 基准测试与系统

自动定理证明系统的质量受益于大规模标准基准测试库——TPTP（Thousands of Problems for Theorem Provers）问题库。此外，自动演绎会议（CADE）每年举办CADE ATP系统竞赛（CASC），选用TPTP库中的题目进行评比。重要的ATP系统包括：E（基于纯等式演算的高性能证明器）、Vampire（自2001年以来多次赢得CASC冠军）、SPASS（一阶逻辑带等式证明器）、Prover9（接替Otter的证明器）以及Z3（兼作SMT求解器）。
拉塞尔县 (亚拉巴马州)

<image>

拉塞尔县（Russell County）是位于美国亚拉巴马州东部的一个县，县治凤凰城。根据美国人口调查局2000年统计，共有人口49,756，其中白人占56.69%、非裔美国人占40.84%。

## 地理

根据美国人口调查局的数据，该县的总面积为647平方英里（1,680平方公里），其中641平方英里（1,660平方公里）为陆地，6.1平方英里（16平方公里，0.9%）是水，该县位于海湾沿海平原地区，由于靠近美国东部的秋季线，有一些起伏的丘陵。
公共陆基移动网

公共陆基移动网（Public land mobile network，或简称“PLMN”，大陆：公共陆地移动网络、公众陆地移动电话网、公用陆地移动网络、公用陆地移动通信网、公共陆基移动网；台湾：公众陆地行动网、陆地移动电话网络、公用陆上移动网络、公众移动电话网络；香港：公地流动网络）是一电子通讯术语，为基于陆地、必须装备无线电发射台（发射塔）与基地台的移动电话设施的总称，与其他公共陆基移动网络、提供电话通讯的交换网、传送数据和提供因特网服务的服务商实现互联。

PLMN由移动设备国家代码（MCC）和移动设备网络代码（MNC）标识。每个运营商都有其自己的PLMN。

## 公共交换电话网

公用陆上移动网络需要连线到公共交换电话网络（PSTN）才能将数据网络路由到通话网络。就跟互联网是全球公众IP的封包交换网络相似，PSTN是由一群语音为主的通话网络相互连结的大网络，它可以是私有或是国有。电路交换的电话网络从亚历山大·格拉汉姆·贝尔发明电话之后已经有相当大的进步，而且在20世纪末除了部分本地回路端分机系统以外几乎已经第七号发信系统化了，而且PSTN也从固定式的电话扩充至移动式系统。

而且PSTN也提供了长距离互联网的基础架构以及使用者的这两个条件。

因为互联网服务提供商（ISP）支付长途电话营运商来存取他们的基础设施，并通过分封交换将电路分享给许多用户使用，互联网使用者就能避免支付使用费给不属于他们的ISP。

许多观察家认为PSTN的远程规划是成为互联网的其中一种应用，不过在此目标达成之前，互联网需要做一些修改才能实际应用。像是需要应用QoS才能够提升VoIP技术的通话品质。

PSTN的技术已经被ITU-T大量的标准化，使用的是E.163/E.164位址（通常称之电话号码）定址。另外有大量的私有电话网络没有连线到PSTN，大部分是用于军事用途。也有一些私有电话网络是在大型公司内运作，然后借由电话分机系统连线至PSTN。

## 架构

- 载送服务：此服务提供用户发送讯息至特定的存取点所需的能力。
- 远程服务：提供用户利用终端设备功能与其他用户进行通信的必要条件。
- 补充业务：修改或补充基础电信服务及提供共同或相关的基础通信服务。

## 外部链接

- Federal Standard 1037C（1996）
- GSM Overview
朗兹县 (亚拉巴马州)

<image>

朗兹县（Lowndes County）是位于美国亚拉巴马州中南部的一个县，县治海恩维尔。根据美国人口调查局2000年统计，共有人口13,472，其中非裔美国人占73.37%、白人占25.86%。
梅肯县 (亚拉巴马州)

<image>

梅肯县（Macon County）是位于美国亚拉巴马州中东部的一个县，县治塔斯基吉。根据美国人口调查局2000年统计，共有人口24,105，其中非裔美国人占84.64%、白人占13.96%。
插水 (足球术语)

假摔，香港称为插水（Diving 或 simulation）是一个足球术语。意思是指一个球员为了博取自由球或点球等罚球，而假装被对手侵犯倒地，由于不少球员假装被侵犯时，会自行跌倒在地，动作近似跳水运动的入水动作，故英文称为Diving。

决定一个球员是否假摔，亦是一个有争议性的足球话题。很多足球迷特别是英国球迷，会视插水为欺骗行为。值得一提的是，球迷通常会对自己拥戴的球员的假摔行为持支持态度。

## 惩罚

插水动作最初只是一个关乎比赛道德的问题，但后来问题越来越严重，也影响球证执法，国际足协正式将插水行为定为违规行为，球证会判罚插水的一方，并给予对手自由球；如借此获得十二码，亦可能会被视像助理裁判取消。而一般球证会发出黄牌以作警告插水球员。

## 假摔事件

1998年世界杯半准决赛，阿根廷对荷兰的比赛，阿根廷前锋柯迪加突破荷兰防线后在禁区内“插水”博十二码，被球证出示黄牌警告。此时愤怒的荷兰门将云达沙冲前破口大骂；心有不甘的柯迪加立即站起来并企图以头锤攻击云达沙的下腭，后者回以“假摔”应声倒地，前者即立即领红牌被逐离场。后来，荷兰在一次反击中得手，将阿根廷淘汰出局。

2000年欧洲杯，在罗马尼亚对阵意大利的比赛中，罗马尼亚前锋格奥尔基·哈吉在禁区中倒地企图骗取点球，被主裁判出示第二张黄牌罚下。

2002年世界杯，巴西在分组赛对土耳其的赛事中，当时巴西队正在领先，巴西中场里瓦尔多在一次攻势中主踢角球，土耳其的后卫把球踢给里瓦尔多，原意是为了要他早点开球以免浪费时间，球只是碰到里瓦尔多的脚，但里瓦尔多却立即掩面倒地，并在场中假装面部受伤的痛苦状，躺了数分钟，结果当时看不见此情况的球证立即出示红牌将该名土耳其球员驱逐出场，巴西最终以2:1胜土耳其。事后里瓦尔多被国际足联以不君子行为重罚，但李华度却解释掩面是为了保护自己，怕被球打中头部。

2014年世界杯，阿扬·罗本在十六强对阵墨西哥，比赛中三次假摔，第三次假摔于完场前，成功于补时期间为球队搏得十二码，助球队2:1反胜墨西哥。罗本赛后承认比赛期间倒地太明显：“有一次（最终变成）十二码，对方进入禁区，我就轻易地摔倒，我不应该那样。”罗本因使用假摔来赚取十二码机会遭到记者广泛谴责而出名。

2018年世界杯，巴西对上哥斯达黎加的比赛中，前锋内马尔曾以假摔试图博取发球，其行为甚至于地上翻滚好几圈，这件事在事后被大幅报导并有大量恶搞影片出现于网络。

2026年世界杯，埃及对上阿根廷的比赛中，埃及前锋穆罕默德·萨拉赫第91分钟与阿根廷球员朱利安·艾瓦雷兹在阿根廷禁区拼抢球权时故意引导观众与裁判认定其被犯规，实则为假摔为骗取点球，随着后来球权被转移至阿根廷球员并导致随后阿根廷成功反击逆转比分后，引发埃及方面抗议表示不满，随后也在社交媒体引发争议。

2026年世界杯，瑞士与阿根廷的八强淘汰赛中恩博洛与帕雷德斯争球权，前者顺势倒地，但经VAR检视为假摔，恩博洛被判第二张黄牌，最终拿红牌下场。
马伦戈县

<image>

马伦戈县（Marengo County）是位于美国亚拉巴马州中西部的一个县，县治林登。根据美国人口调查局2000年统计，共有人口22,539，其中非裔美国人占51.71%、白人占47.28%。
马歇尔县 (亚拉巴马州)

<image>

马歇尔县（Marshall County）是位于美国亚拉巴马州东北部的一个县，县治甘特斯维尔。根据美国人口调查局2000年统计，人口为82,231，其中白人占93.38%、非裔美国人占1.47%。