终止证明方法在形式化建模中的应用

随着形式化方法的普及和应用,定理证明器HOL4在形式化建模过程中无法自动完成终止证明的情况越来越多,而手动终止证明又缺少通用的证明思路.针对这种情况,提出规范化的手动终止证明方法.该方法从问题产生的本质入手,首先保证目标具备解决终止问题的必要条件,然后通过等效替换简化证明目标,最后以原有定理库为基础,寻找证明过程中缺失的引理,推进证明.实例表明,该方法逻辑清晰,能够有效地解决HOL4中大部分情况下的手动终止证明问题.

齐次F5算法的简单终止性证明

自从F5算法提出以来,出现了一批基于标签的Gr?bner基算法,它们使用了不同的选择策略且减少冗余多项式的准则也各不相同。为了满足正确终止性,这些算法的策略和准则必须满足一些一般的规律。根据这些规律,该文提出了一个框架,使大多数算法成为该框架的实例。随后,利用重写基的性质,得到了框架的简单正确终止证明。为了得到F5算法的简单证明,该文对F5算法的约化操作进行合理的化简。特别地,对于齐次F5算法,证明了其复杂的选择策略等价于按模序选择。这样,齐次F5算法就能看成框架的一个特例,从而得到了F5算法的简单证明。

对“就业黑名单”现象的法律思考

"就业黑名单"是一种针对特定劳动者的就业歧视行为,制作、发布"就业黑名单"侵犯了劳动者的劳动权。现行法律对此未纳入司法程序予以救济,劳动者以名誉侵权为由要求用人单位赔偿损失被证明难以成为一个可靠的救济方式。劳动关系终止后应对劳动者负有保护义务,关于劳动者信息的采集、使用、公开,应予以严格限制。制作、公布"就业黑名单",用人单位应对劳动者承担惩罚性赔偿金,招聘单位对此类劳动者在求职时存在歧视,应承担适当赔偿责任。