论文部分内容阅读
73构形的存在性是有限几何中的一个基本问题。本文给出了一种用Alloy分析器自动验证73构形的存在性的方法。该方法使用 Alloy语言对Fano提出的公理系统和需要验证的定理进行形式化,然后利用Alloy分析器分析定理是否满足属性要求。实验结果表明本文提出的机器验证方法是可行的。
基于Alloy的7<sub>3</sub>构形存在性定理的机器验证
【摘 要】
：
73构形的存在性是有限几何中的一个基本问题。本文给出了一种用Alloy分析器自动验证73构形的存在性的方法。该方法使用 Alloy语言对Fano提出的公理系统和需要验证的定理进行
【机 构】
：
辽宁师范大学数学学院,大连市第二十四中学
【出 处】
：
应用数学进展
【发表日期】
：
2017年8期
其他文献
近年来我国P2P网络借贷平台处于快速发展阶段,截止2015年8月成交量达到974.63亿元,但平台信用风险已经凸显,持续出现倒闭现象,能否有效识别借款者并控制其信用风险直接影响P2
渤海湾是受风暴潮灾害影响最严重的地区,在夏季容易遭受台风风暴潮,在春秋和冬春过渡季节,容易遭受温带风暴潮的袭击。近十年来,渤海大量围填海工程建设,使渤海湾岸线变化明
目的探讨儿童肾小球肾炎患者血清cystatin C（Cys C）水平与肾功能损害程度之间关系。方法血清Cys C采用乳微粒子增强比浊法测定,血尿素氮（BUN）采用动力学紫外法测定,血肌酐（sCr）采用
本文根据HIV在感染者体内的感染过程,建立具有Logistic增长、药物治疗和潜伏感染的HIV动力学模型来模拟感染过程中病毒颗粒、T细胞和药物治疗之间的相互关系;然后运用微分方
文章分析了车道占用对城市交通能力的影响,在实验视频数据基础上建立方差分析模型和基于微分方程的多元回归模型,并对结果进行定性分析和定量计算。首先,通过观察案例视频得
目的为了进一步阐明脑电生物反馈治疗注意缺陷多动障碍（ADHD）的可能作用机制,探讨脑电生物反馈处理对ADHD动物模型自发性高血压大鼠（SHR）的行为学和纹状体即早期基因fosB表达的影
我们首先利用行波约化法将一类KdV型方程约化为常微分方程,然后运用指数函数法,并借助于数学软件Mathematica,获得了该方程丰富的精确解析解,并绘制解的图像。
本文首先介绍一般多元高斯分布,包括随机向量高斯分布和随机矩阵高斯分布,研究了其基本性质,重点引进随机张量高斯分布,并研究了随机张量高斯分布的基本性质。
孤立子,混沌和分形是非线性科学的重要组成部分,在上世纪得到了极大的发展。在非线性科学的创立和发展过程中,Fermi-Pasta-Ulam (FPU)问题扮演着及其关键的作用。本文首先简
本文首次研究了环境污染下一类具有尺度结构的种群系统的最优控制问题,通过控制种群的收获和外界毒素向环境的输入率使得人们的总收益最大。利用不动点定理得到了系统解的存