基于边权重图神经网络的一阶逻辑前提选择

刘清华; 徐扬; 吴贯锋; 李瑞杰

doi:10.3969/j.issn.0258-2724.20210134

基于边权重图神经网络的一阶逻辑前提选择

doi: 10.3969/j.issn.0258-2724.20210134

刘清华^{1, 2,},
徐扬^{2, 3, ,},
吴贯锋^{2, 3},
李瑞杰⁴

1.
西南交通大学信息科学与技术学院，四川成都 611756
2.
西南交通大学系统可信性自动验证国家地方联合工程实验室，四川成都 610031
3.
西南交通大学数学学院，四川成都 611756
4.
西南交通大学交通运输与物流学院，四川成都 611756

基金项目: 中央高校基本科研业务费专项资金（2682020CX59，2682021CX057）；教育部人文社会科学研究项目（20XJCZH016，19YJCZH048）；四川省科技计划（2020YJ0270，2020YFH0026）

详细信息

作者简介:
刘清华（1992—），女，博士研究生，研究方向自动推理、智能信息处理，E-mail：qhliu@my.swjtu.edu.cn

通讯作者:
徐扬（1956—），男，教授，博士，研究方向为逻辑代数、不确定性推理和自动推理，E-mail：xuyang@home.swjtu.edu.cn

中图分类号: TP391
计量
- 文章访问数: 487
- HTML全文浏览量: 292
- PDF下载量: 36
- 被引次数: 5
出版历程
- 收稿日期: 2021-02-23
- 修回日期: 2021-07-12
- 网络出版日期: 2022-08-24
- 刊出日期: 2021-11-17

Edge-Weighted-Based Graph Neural Network for First-Order Premise Selection

LIU Qinghua^{1, 2
,},
XU Yang^{2, 3
, ,},
WU Guanfeng^{2, 3},
LI Ruijie⁴

1.
School of Information Science and Technology, Southwest Jiaotong University, Chengdu 611756, China
2.
National-Local Joint Engineering Laboratory of System Credibility Automatic Verification, Southwest Jiaotong University, Chengdu 610031, China
3.
School ofMathematics, Southwest Jiaotong University, Chengdu 611756, China
4.
School of Transportation and Logistics, Southwest Jiaotong University, Chengdu 611756, China

摘要

摘要:
为提高自动定理证明器在大规模问题中证明问题的能力，前提选择任务应运而生. 由于公式图的有向性，主流的图神经网络框架只能单向地对节点进行更新，且无法编码公式图中子节点间的顺序. 针对以上问题，提出了带有边类型的双向公式图表示方法，并提出了一种基于边权重的图神经网络（edge-weight-based graph neural network，EW-GNN）模型用于编码一阶逻辑公式. 该模型首先利用相连节点的信息来更新对应边类型的特征表示，随后利用更新后的边类型特征计算邻接节点对中心节点的权重，最后利用邻接节点的信息双向地对中心节点进行更新. 实验比较分析表明：基于边权重的图神经网络模型在前提选择任务中表现得更加优越，其在相同的测试集上比当前最优模型的分类准确率高了约1%.
- 图神经网络 /
- 双向图 /
- 前提选择 /
- 一阶逻辑公式
Abstract:
In order to improve the ability of automated theorem provers, the premise selection task emerges. Due to the directional nature of formula graphs, most current graph neural networks can only update nodes in one direction, and cannot encode the order of sub-nodes in the formula graph. To address the above problems, a bidirectional graph with edge types to represent logical formulae and a edge-weight-based graph neural network (EW-GNN) model to encode first-order logic formulae are proposed. The model firstly uses the information of connected nodes to update the feature representation of the corresponding edge type, then calculates the weight of the adjacent node to the central node with the updated edge type feature, and finally uses the information of the adjacent node to update the target node in both directions. The experimental results show the edge-weighted-based graph neural network model performs better in the premise selection task, which can improve the classification accuracy by 1% compared to the best model on the same test dataset.
- graph neural network /
- bidirectional graph /
- premise selection /
- first-order logical formula

HTML全文

单箱双室箱梁在城市桥梁和公路桥梁中应用广泛. 采用该截面形式桥梁的箱体和桥面宽度较大，在竖向荷载作用有偏心时，其畸变效应不同于单箱单室箱梁. 箱梁的畸变效应研究文献较多，一般采用能量变分法或板元分析法都可得到一个四阶控制微分方程，方程未知量为畸变角或箱梁梁肋挠度w，都能很好地揭示单箱单室箱梁的畸变效应.

张元海等^[1]采用能量变分原理对单箱单室箱梁的畸变效应进行了研究，分析了双层悬臂板对畸变的影响；徐勋等^[2-3]采用广义坐标法研究了单箱单室箱梁的畸变；王兆南等^[4]采用板元分析法研究了单箱单室箱梁的畸变效应；Pezeshky等^[5]研究了宽翼缘钢梁的畸变. 单箱单室简支直线箱梁畸变的研究文献较多，成果较多. 曲线箱梁因扭转、弯曲和畸变相互耦合，畸变研究较为复杂^[6-8]. 畸变的试验研究可对畸变理论分析结果进行验证：刘保东等^[9]对连续刚构桥的扭转和畸变进行了试验研究；狄瑾等^[10]对波形钢腹板组合箱梁的扭转和畸变进行了试验研究，分析了扭转、畸变和弯曲正应力的占比. 波形钢腹板组合箱梁由于结构自重轻，适合大跨度桥梁的设计，其畸变也比混凝土箱梁明显^[11]，畸变研究也较深入. Li等^[12-14]研究了变截面箱梁的畸变，不同于求解常截面箱梁畸变控制微分方程常采用的初参解法，而采用纽马克法求解变截面箱梁的畸变控制微分方程. 双室箱梁桥的畸变不同于单室箱梁桥，蔺鹏臻等^[15]研究了单箱双室箱梁对称弯曲时的局部扭转效应；Chidolue等^[16]研究了多室箱梁的扭转和畸变，多数文献在研究双室箱梁的畸变效应时，只考虑反对称畸变，而忽略了正对称畸变.

单箱双室箱梁相比单箱单室箱梁增加了一道腹板，这使得在偏心竖向荷载作用下，箱梁畸变不仅有反对称畸变，还存在正对称畸变. 若忽略正对称畸变，在理论上将不完善，计算结果误差也较大，且双室箱梁在得出畸变翘曲惯性矩，框架横向抗弯惯性矩时也不同于单箱单室箱梁. 由于有两种畸变模式，因此无法采用一个微分方程来描述畸变效应，需采用两个未知量，对应两个微分方程才能完整描述单箱双室箱梁的畸变效应. 本文从单箱双室箱梁的畸变荷载分析出发，以箱梁的畸变角γ_d为未知量，定义正、反对称畸变对应的畸变角，建立正、反对称畸变的四阶控制微分方程，以揭示单箱双室箱梁的畸变效应，为单箱双室箱梁桥的设计计算提供参考.

1. 基本假定和畸变荷载

在薄壁箱梁畸变基本理论假定^[1]的基础上，结合单箱双室箱梁在偏心荷载作用下的位移变形和实际设计需考虑的因素等，补充矩形截面单箱双室箱梁畸变分析的假定：单箱双室箱梁的边腹板厚度相同，箱梁横向变形时角点的转角位移可忽略.

单箱双室箱梁一般都会存在一个对称轴y，箱梁截面尺寸如图1所示. 图1中：d、a₁、a₂分别为悬臂板、腹板、顶板（底板）的宽度；t₁、t₂、t₃、t₄、t_h分别为腹板AD、底板、腹板BC、顶板、腹板KF的厚度；e为荷载偏心距；P为单箱双室箱梁顶板上线性分布的偏心竖向荷载 . 采用右手坐标系，O为原点. 箱梁截面各角点分别采用A、B、C、D、K、F表示.

图 1 单箱双室箱梁截面形式

Figure 1. Cross section of single box double-cell box girder

下载: 全尺寸图片幻灯片

如图1所示，沿梁纵向取单位长框架后，P可等效成一力矩Pe和一作用于K点的竖向力P. 力矩可分解出使箱梁发生反对称畸变的荷载 $P_{}e/{a_2}$ ，竖向力P可分解出使箱梁发生正对称畸变的荷载 $P/3$ 和 $2P/3$ ，如图2所示. 畸变正应力可对应叠加，继续分解的畸变荷载如式（1）所示.

图 2 正对称和反对称畸变荷载

Figure 2. Positive-symmetrical and antisymmetrical distortion load

下载: 全尺寸图片幻灯片

$\left\{ \begin{gathered} {P_{41}} = {P_{42}} = {P_{21}} = {P_{22}} = P_{}e/(8{a_1}), \\ {P_{11}} = {P_{12}} = {P_{31}} = {P_{32}} = P_{}e/(4{a_2}), \\ {R_{41}} = {R_{42}} = {R_{21}} = {R_{22}} = P_{}{a_2}/(6{a_1}), \\ {R_{11}} = {R_{12}} = {R_{31}} = {R_{32}} = P_{}/3, \\ \end{gathered} \right.$

(1)

式中： ${P_{41}}$ 、 ${P_{42}}$ 、 ${P_{12}}$ 、 ${P_{22}}$ 、 ${P_{21}}$ 、 ${P_{11}}$ 、 ${P_{31}}$ 和 ${P_{32}}$ 为反对称畸变荷载； ${R_{41}}$ 、 ${R_{42}}$ 、 ${R_{12}}$ 、 ${R_{22}}$ 、 ${R_{21}}$ 、 ${R_{11}}$ 、 ${R_{31}}$ 和 ${R_{32}}$ 为正对称畸变荷载.

2. 单箱双室箱梁反对称畸变

采用板元分析法研究单箱双室箱梁的反对称畸变，可得出箱梁的畸变翘曲刚度、框架横向抗弯刚度和畸变荷载之间的关系. 箱梁发生反对称畸变时，σ_dA和σ_dD为箱梁角点A、D的畸变正应力，令β₁= σ_dA/σ_dD，畸变正应力在各板件上的分布如图2所示. β₁可由各板件上的畸变正应力合成的对坐标轴力矩之和为0的条件求得.

2.1 各板元面内力系分析

沿梁纵向取一微段，离散各板件，如图3所示. 图中：q_xB、q_xA、q_xK为箱梁腹板对顶板的横向约束反力；T_odz为微段上腹板对顶板的纵向约束反力；Q_o、M_o分别为顶板上产生的面内剪力和力矩；q_xC、q_xD、q_xF为腹板对底板的横向约束反力；T_udz为腹板对底板的纵向约束反力；Q_u、M_u分别为底板上产生的面内剪力和力矩；q_yA、q_yD分别为箱梁顶板和底板对左腹板的横向约束反力；Q_c、M_c分别为左腹板面内剪力和力矩.

图 3 箱梁各板件的面内受力

Figure 3. In-plane force of box girder plates

下载: 全尺寸图片幻灯片

由顶板、底板和腹板的面内力矩平衡，顶板和底板面内沿x轴，腹板面内沿y轴方向列取力系平衡方程. 考虑到各板件之间在畸变荷载作用下维持力系平衡状态，略去高阶微量后得出：

$\begin{split} & \frac{{{{\rm{d}}^2}{M_{\text{c}}}}}{{{\rm{d}}{{\textit{z}}^2}}} + \frac{{{a_1}}}{{2{a_2}}}\left(\frac{{{{\rm{d}}^2}{M_{\rm{o}}}}}{{{\rm{d}}{{\textit{z}}^2}}} + \frac{{{{\rm{d}}^2}{M_{\text{u}}}}}{{{\rm{d}}{{\textit{z}}^2}}}\right) + \frac{{{a_1}({P_{41}} + {P_{21}})}}{{{a_2}}} \;+\\ &\quad {P_{11}} - \left[\frac{{{a_1}({q_{{\rm{x}}1}} + {q_{{\rm{x}}2}})}}{{2{a_2}}} + {q_{\rm{y}}}\right] = 0 , \end{split}$

(2)

式中： $q_{\mathrm{x} 1}=q_{\mathrm{x}A} + q_{\mathrm{x}B} + q_{\mathrm{x}K}$ ， $q_{\mathrm{x}K}$ 作用在板件AB的跨中，方向和 $q_{\mathrm{x}A}$ 相同； $q_{\mathrm{x} 2}=q_{\mathrm{x}C} + q_{\mathrm{x}D} + q_{\mathrm{x}F}$ ， $q_{\mathrm{x}F}$ 作用在板件CD的跨中，方向和 $q_{\mathrm{x}C}$ 相同； $q_{\mathrm{y}}=q_{\mathrm{y}A} + q_{\mathrm{y}D}$ .

箱梁在反对称畸变时各角点的位移如图4所示，图中：Δ_HA、Δ_HB、Δ_HC、Δ_HD为对应各角点水平位移；Δ_VA、Δ_VB、Δ_VC、Δ_VD为对应各角点竖向位移；α₁、α₂、α₃为对应各板件畸变后的角度改变.

图 4 箱梁各角点的位移

Figure 4. Corner displacements of box girder

下载: 全尺寸图片幻灯片

定义单箱双室箱梁反对称畸变的畸变角γ_d1为

${\gamma _{{\rm{d1}}}} = \frac{{{\alpha _1} + {\alpha _2}}}{2} + {\alpha _3}{\text{ = }}\frac{{{\varDelta _{{\rm{V}}A}} + {\varDelta _{{\rm{V}}D}}}}{{{a_2}}} + \frac{{{\varDelta _{{\rm{H}}D}} + {\varDelta _{{\rm{H}}A}}}}{{{a_1}}}.$

(3)

各板件上的力矩M_o、M_u、M_c之间存在对应关系^[4]. 对γ_d1关于z轴求二次微分后，考虑到箱梁各角点位移和面内力矩的关系^[1]，得到

${\gamma ''_{{\rm{d1}}}} = - \frac{{4{M_{\text{c}}}}}{{{a_2}E{J_1}}},$

(4)

式中：E为材料弹性模量；J ₁为腹板 AD （腹板 BC ）的面内惯性矩.

对式（4）再求二次微分后，可将式（2）化简为

$\begin{split} & - E\frac{{a_2^2{J_1}(1 + {\beta _1}) + a_1^2({\beta _1}{J_4} + {J_2})}}{{4{a_2}(1 + {\beta _1})}}{\gamma^{(4)}_{{\rm{d}}1}} +\\ &\quad \frac{{{a_1}}}{{{a_2}}}({P_{41}} + {P_{21}}) + {P_{11}} - \left[\frac{{{a_1}({q_{{\rm{x}}1}} + {q_{{\rm{x}}2}})}}{{2{a_2}}} + {q_{\rm{y}}}\right] = 0, \end{split}$

(5)

式中：J_n=t_n $a_n^3$ /12 (n=1,2)，J₄=t₄ (a₂ + 2d)³/12，J₂、J₄分别为底板、顶板的面内惯性矩.

2.2 各板元面外力系分析

采用箱梁各板件的面外力系分析化简式（5）中的 ${a_1}({q_{{\rm{x}}1}} + {q_{{\rm{x}}2}})/(2{a_2}) + {q_{\rm{y}}}$ 项. 在分析过程中考虑箱梁腹板KF对框架横向抗弯惯性矩的贡献，单箱双室箱梁在反对称荷载作用下发生畸变后，离散箱梁各板件，各板件的面外受力如图5所示，图中变量m_AK、m_AD等为各板件板端的畸变横向弯矩.

图 5 反对称畸变时各板件的面外受力

Figure 5. Out-of-plane force with antisymmetrical distortion

下载: 全尺寸图片幻灯片

反对称畸变时，取出板件AK和DF分析面外受力可得： ${q_{{\rm{y}}A}}{a_2} = 2({m_{AK}} + {m_{KA}})$ ， ${q_{{\rm{y}}D}}{a_2} = 2({m_{DF}} + {m_{FD}})$ . 取出板件AD和BC分析面外受力可得： ${q_{{\rm{x}}A}}{a_1} = {m_{AD}} + {m_{DA}}$ ， ${q_{{\rm{x}}B}}{a_1} = {m_{BC}} + {m_{CB}}$ ， ${q_{{\rm{x}}A}} = {q_{{\rm{x}}D}}$ ， ${q_{{\rm{x}}B}} = {q_{{\rm{x}}C}}$ . 取出板件KF分析面外受力可得： ${q_{{\rm{x}}K}}{a_1} = {m_{KF}} + {m_{FK}} - {m_{KA}} - {m_{KB}} - {m_{FC}} - {m_{FD}}$ .

板件KB和FC的面外力系分析和板件AK等相同. 为得出各板件的板端畸变横向弯矩和板端位移的关系，可采用力矩分配法进行分析，见式（6）.

$\left\{ \begin{gathered} {m_{{{AK}}}} = \frac{{24E{I_4}{i_1}}}{{a_2^2({i_1} + {i_4})}}{\varDelta _{\rm{V}}} + \frac{{12E{I_1}{i_4}}}{{a_1^2({i_1} + {i_4})}}{\varDelta _{\rm{h}}}, \\ {m_{{{AD}}}} = - \frac{{12E{I_1}{i_4}}}{{a_1^2({i_1} + {i_4})}}{\varDelta _{\rm{h}}} - \frac{{24E{I_4}{i_1}}}{{a_2^2({i_1} + {i_4})}}{\varDelta _{\rm{V}}}, \\ {m_{{{DF}}}} = \frac{{24E{I_2}{i_1}}}{{a_2^2({i_1} + {i_2})}}{\varDelta _{\rm{V}}} + \frac{{12E{I_1}{i_2}}}{{a_1^2({i_1} + {i_2})}}{\varDelta _{\rm{h}}}, \\ {m_{{{DA}}}} = - \frac{{12E{I_1}{i_2}}}{{a_1^2({i_1} + {i_2})}}{\varDelta _{\rm{h}}} - \frac{{24E{I_2}{i_1}}}{{a_2^2({i_1} + {i_2})}}{\varDelta _{\rm{V}}}, \\ {m_{{{KA}}}} = \frac{{24E{I_4}{i_{\rm{h}}}}}{{a_2^2(2{i_4} + {i_{\rm{h}}})}}{\varDelta _{\rm{V}}} + \frac{{12E{I_{\rm{h}}}{i_4}}}{{a_1^2(2{i_4} + {i_{\rm{h}}})}}{\varDelta _{\rm{h}}}, \\ {m_{{{FD}}}} = \frac{{24E{I_2}{i_{\rm{h}}}}}{{a_2^2(2{i_2} + {i_{\rm{h}}})}}{\varDelta _{\rm{V}}} + \frac{{12E{I_{\rm{h}}}{i_2}}}{{a_1^2(2{i_2} + {i_{\rm{h}}})}}{\varDelta _{\rm{h}}}, \\ \end{gathered} \right.$

(6)

式中：i₁、i₂、i₄、i_h分别为箱梁边腹板、底板、顶板和中腹板的线刚度；I₁、I₂、I₄、I_h分别为箱梁边腹板、底板、顶板和中腹板的面外惯性矩；Δ_V、Δ_h分别为板件板端竖向位移和水平位移.

在 ${a_1}({q_{{\rm{x}}1}} + {q_{x2}})/(2{a_2}) + {q_{\rm{y}}}$ 中代入q_x1、 q_x2、 q_y的表达式，结合式（6），考虑到式（3）中有Δ_V = Δ_VA =Δ_VD，Δ_h = Δ_HD = Δ_HA，得到

$\begin{split} & \frac{a_{1}\left(q_{\mathrm{x} 1}+q_{\mathrm{x} 2}\right)}{2 a_{2}}+q_{\mathrm{y}}=\frac{48 E}{a_{2}}\left(\frac{I_{\mathrm{h}} I_{4}}{4 I_{4} a_{1}+I_{\mathrm{h}} a_{2}}\;+\right. \\ &\quad \left.\frac{I_{\mathrm{h}} I_{2}}{I_{\mathrm{h}} a_{2}+4 I_{2} a_{1}}+\frac{I_{1} I_{4}}{I_{1} a_{2}+2 I_{4} a_{1}}+\frac{I_{1} I_{2}}{I_{1} a_{2}+2 I_{2} a_{1}}\right) \gamma_{\mathrm{d} 1}. \end{split}$

(7)

将 ${P_{41}}$ 、 ${P_{21}}$ 、 ${P_{11}}$ 代入式（5）中的 $\dfrac{{{a_1}}}{{{a_2}}}({P_{41}} + {P_{21}}) \;+ {P_{11}}$ 项，化简得到 $P_{}e/(2{a_2})$ .

2.3 反对称畸变控制微分方程

根据以上分析可将式（5）化简为单箱双室箱梁在偏心竖向荷载作用下，以反对称畸变角γ_d1为未知量的四阶畸变控制微分方程，如式（8）.

$E{I_{{{{\text{ω}} {\rm{d}}1}}}}{\gamma ^{(4)}_{{\rm{d}}1}} + E{I_{{\rm{R}}1}}{\gamma _{{\rm{d}}1}} = P_{}e/2 ,$

(8)

式中：I_ωd1为单箱双室箱梁反对称畸变的翘曲惯性矩，单位m⁶，如式（9）；I_R1为单箱双室箱梁反对称畸变的横向抗弯惯性矩，单位m²，如式（10）.

${I_{{\text{ω}} {\rm{d}}1}}{\rm{ = }}\frac{{a_2^2(1 + {\beta _1}){J_1} + a_1^2({\beta _1}{J_4} + {J_2})}}{{4(1 + {\beta _1})}},$

(9)

$\begin{split} &I_{\mathrm{R} 1}=48\left(\frac{I_{\mathrm{h}} I_{4}}{4 I_{4} a_{1}+I_{\mathrm{h}} a_{2}}+\frac{I_{\mathrm{h}} I_{2}}{I_{\mathrm{h}} a_{2}+4 I_{2} a_{1}}\;+\right. \\ &\quad \left.\frac{I_{1} I_{4}}{I_{1} a_{2}+2 I_{4} a_{1}}+\frac{I_{1} I_{2}}{I_{1} a_{2}+2 I_{2} a_{1}}\right). \end{split}$

(10)

3. 单箱双室箱梁正对称畸变

3.1 正对称畸变时箱梁畸变翘曲惯性矩

如图2所示，单箱双室箱梁在正对称畸变荷载作用下，产生正对称畸变翘曲变形. 按假定，畸变正应力在各板件上呈线性分布，关于y轴正对称. 考虑到变形亦呈正对称，顶板和底板有竖向位移，而水平位移很小几乎可以忽略，因此可采用一半结构AKFD进行分析，如图6所示，图中：h为箱梁高度. 考虑结构AKFD各角点角位移不相等的情况，当箱梁各板件厚度各不相等时，现有单箱单室箱梁畸变微分方程将不再适用，因按照假定和分析过程，其都建立在箱梁截面至少关于一个坐标轴对称的基础上.

图 6 箱梁正对称畸变扇性坐标ω_d

Figure 6. Positive-symmetrical distortion sector coordinates ω_d

下载: 全尺寸图片幻灯片

采用一个参数β₁描述畸变正应力在各板件上分布的模式不再满足箱梁各板件厚度都不同的情形. 现采用两个参数β₁和β₂分别描述畸变正应力在腹板、顶板（底板）上的分布. 对各板件厚度都不同的箱梁结构，令β₂=σ_dA/σ_dK （σ_dK为箱梁角点 K 的畸变正应力），认为由畸变正应力引起的面内力矩分布在顶、底板上的反弯点位置相同，但不再二等分. 在求出β₁和β₂后，可确定各板件厚度都不同的箱梁的畸变翘曲位移模式.

β₁和β₂可由各板件面内畸变正应力对x、y轴形成的力矩之和为0的条件，且联立式（11）、（12）求得.

${\beta _1}{\text{ = }}\frac{{2{t_2}{a^3}(\beta _2^2 + 1 - {\beta _2}) + 3{a^2}h({t_1}\beta _2^2 + {t_{\rm{h}}})}}{{{\varGamma _1} + {\varGamma _2}}},$

(11)

${\beta _2} = \frac{{3{t_4}\beta _1^2({a^2} - {d^2}) + 3{t_2}{a^2} + 2ah{t_{\rm{h}}}(\beta _1^2 + 1 - {\beta _1})}}{{3{t_4}\beta _1^2{{(a + d)}^2} + 3{t_2}{a^2} + 2ah{t_1}(\beta _1^2 + 1 - {\beta _1})}},$

(12)

式中：a为分割后单箱的顶板或底板宽度； ${\varGamma _1} = 2{t_4}(a + d)[(\beta _2^2 - {\beta _2} + 1){a^2} + {d^2}{({\beta _2} + 1)^2}]$ ； ${\varGamma _2} = 2{t_4}(a + d)\times ad(2\beta _2^2 + {\beta _2} - 1) + 3{a^2}h({t_1}\beta _2^2 + {t_{\rm{h}}})$ .

求得β₁、β₂后，根据 ${I_{\text{ω}{\rm{ d}}}} = \displaystyle\int_S {\omega _{\rm{d}}^2{\rm{d}}S}$ 可求得结构AKFD的畸变翘曲惯性矩I_ωd2，如式（13）所示，S为板件截面积.

$\begin{split} & {I_{{\text{ω}} {\rm{d}}2}} = \frac{{{h^2}{t_4}\beta _1^2[{{({\beta _2}a +{\beta _2}d + d)}^3} + {a^3}]}}{{48\beta _2^2(1 + {\beta _2}){{(1 + {\beta _1})}^2}}} + \\ &\quad \frac{{{h^2}{t_2}{a^3}(\beta _2^3 + 1)}}{{48\beta _2^2(1 + {\beta _2}){{(1 + {\beta _1})}^2}}} + \frac{{({t_{\rm{h}}} + \beta _2^2{t_1})(\beta _1^3 + 1){a^2}{h^3}}}{{48\beta _2^2{{(1 + {\beta _1})}^3}}}. \end{split}$

(13)

3.2 正对称畸变时框架横向抗弯惯性矩

结构AKFD在正对称畸变荷载作用下发生如图7所示的变形. 在图7中：设定杆件AK和DF杆端的弯矩、转角以逆时针为正；杆件AK和DF皆沿y轴有相同的竖向位移；M_AK、M_KA分别为AK杆件杆端A、K的横向弯矩；γ_d2 = Δ_V/a，为单箱双室发生正对称畸变时的畸变角.

图 7 结构AKFD的变形和横向弯矩

Figure 7. Deformation and transverse bending moment of structure AKFD

下载: 全尺寸图片幻灯片

根据分析，可忽略杆件AD和KF水平x向位移，采用杆件的转角位移公式，可用畸变角γ_d2将角点D的畸变横向弯矩表示出来，有M_DF = I_Dγ_d2. 同理可得其他板件的板端弯矩：M_KA = I_Kγ_d2、 M_AK = I_Aγ_d2、 M_FD = I_Fγ_d2. I_D、I_K、I_A和I_F见式（14），同时可方便地确定结构的横向弯曲应变能.

$\qquad\left\{ \begin{array}{l} {I_{{D}}} = \dfrac{{[(4{\varTheta _1} + {\varTheta _3}){i_2}{i_{\rm{h}}} - 3{\varTheta _1}i_2^2]({\varTheta _2} + 3{\varTheta _1}){i_1}{i_4}} + {{[(6{\varTheta _1} - {\varTheta _2}){i_2}{i_{\rm{h}}} - 3{\varTheta _1}i_2^2][3{\varTheta _1}i_1^2 - (4{\varTheta _1} + {\varTheta _3}){i_1}{i_4}]}}}{{{\varGamma _3}}} ， \\ {I_{{K}}} = \dfrac{{[(4{\varTheta _3} + {\varTheta _1}){i_1}{i_4} - 3{\varTheta _3}i_4^2]({\varTheta _2} + 3{\varTheta _3}){i_2}{i_{\rm{h}}}} + {{[(6{\varTheta _3} - {\varTheta _2}){i_1}{i_4} - 3{\varTheta _3}i_4^2][3{\varTheta _3}i_{\rm{h}}^2 - (4{\varTheta _3} + {\varTheta _1}){i_2}{i_{\rm{h}}}]}}}{{{\varGamma _4}}} ， \\ {I_{{A}}} = \dfrac{{2({\varTheta _2} + 3{\varTheta _1}){i_1}{i_4}}}{{{\varTheta _3}{i_4} + {\varTheta _1}{i_1}}}， \\ {I_{{F}}} = \dfrac{{2({\varTheta _2} + 3{\varTheta _3}){i_2}{i_{\rm{h}}}}}{{{\varTheta _1}{i_2} + {\varTheta _3}{i_{\rm{h}}}}}， \end{array} \right.$

(14)

式中：参数Θ₁、Θ₂、Θ₃与箱梁各板件线刚度有关； ${\varGamma _3}$ = $[3{\varTheta _1}i_1^2 - (4{\varTheta _1} + {\varTheta _3}){i_1}{i_4}]{\varTheta _1}({i_{\rm{h}}} - {i_2}) +[(4{\varTheta _1} + {\varTheta _3}){i_2}{i_{\rm{h}}} - 3{\varTheta _1}i_2^2] {\varTheta _1} ({i_1} - {i_4})$ ； ${\varGamma _4}$ = $[3{\varTheta _3}i_{\rm{h}}^2 - (4{\varTheta _3} + {\varTheta _1}){i_2}{i_{\rm{h}}}]{\varTheta _3}({i_1} - {i_4}) + [(4{\varTheta _3} + {\varTheta _1}){i_1}{i_4} - 3{\varTheta _3}i_4^2]{\varTheta _3}({i_{\rm{h}}} - {i_2})$ .

3.3 正对称畸变控制微分方程

箱梁的总横向弯曲应变能可表示为 ${u_{\rm{e}}} = \dfrac{1}{2}\displaystyle\int_L {\displaystyle\int_s {\dfrac{{M^2{{(s)}}}}{{EI}}{\rm{d}}s} {\rm{d}}L}$ ，其中：M(s)为箱室各板件周向s处的横向弯矩；I为各板件的面外惯性矩；L为梁长.

沿梁轴z向取单位长框架，可得箱梁各板件的横向弯曲应变能之和，如式（15）所示. 也可写为 $\dfrac{1}{2}E{I_{{\rm{R}}2}}\gamma _{{\rm{d}}2}^2$ ，I_R2为箱室各板件厚度均不相等时的框架横向抗弯惯性矩，如式（16）.

$\begin{split} &u_{{{\rm{e}}}}= \frac{\gamma_{{{\rm{d}}} 2}^{2}}{6 E}\left[\frac{a\left(I_{{A}}^{2}+I_{{K}}^{2}-I_{{A}} I_{{K}}\right)}{I_{4}}+\frac{h\left(I_{{K}}^{2}+I_{{F}}^{2}-I_{{K}} I_{{F}}\right)}{I_{{{\rm{h}}}}}+\right.\\ &\quad \left.\frac{a\left(I_{{{{D}}}}^{2}+I_{{F}}^{2}-I_{{{{D}}}} I_{{F}}\right)}{I_2}+\frac{h\left(I_{{A}}^{2}+I_{{D}}^{2}-I_{{A}} I_{{{{D}}}}\right)}{I_1}\right],\\[-16pt] \end{split}$

(15)

$\begin{split} & I_{\mathrm{R} 2}= \frac{1}{3 E^{2}}\left[\frac{a\left(I_{{A}}^{2}+I_{{K}}^{2}-I_{{A}} I_{{K}}\right)}{I_{4}}+\frac{h\left(I_{{K}}^{2}+I_{{F}}^{2}-I_{{K}} I_{{F}}\right)}{I_{\rm{h}}}+\right.\\ &\quad \left.\frac{a\left(I_{{D}}^{2}+I_{{F}}^{2}-I_{{D}} I_{{F}}\right)}{I_{2}}+\frac{h\left(I_{{A}}^{2}+I_{{D}}^{2}-I_{{A}} I_{{D}}\right)}{I_{1}}\right].\\[-16pt] \end{split}$

(16)

通过以上分析可得，单箱双室箱梁发生正对称畸变时，取一半结构得出的畸变微分方程如式（17）. I_R2单位为m²， ${I_{{\text{ω}}{\rm{d}}2}}$ 单位为m⁶.

$E{I_{{\text{ω}} {\rm{d}}2}}{\gamma ^{(4)}_{{\rm{d}}2}} + E{I_{{\rm{R}}2}}{\gamma _{{\rm{d}}2}} = Pa/3.$

(17)

采用畸变角γ_d1、γ_d2分别描述箱梁的反对称和正对称畸变，得出两个畸变微分方程，方程可采用初参数法或弹性地基梁比拟法进行求解^{[1, 4]}.

4. 数值算例及参数分析

在等高度矩形截面简支箱梁上设置端横隔板，计算跨径L=80 m，截面如图8所示. E=35 GPa，泊松比μ=0. 在箱梁顶板上作用偏心竖向分布力矩1 kN · m/m，箱梁截面关于y轴对称. 采用本文单箱双室箱梁畸变理论进行计算分析，同时去掉中腹板按照单箱单室箱梁计算对比，得到的各畸变数值见表1，表中：B_d为畸变双力矩；ω_dA、ω_dD为角点A、D的畸变扇性坐标. B_d、γ_d的值为弹性地基梁比拟法中单位荷载作用下的计算值，σ_d为实际荷载作用下的值.

图 8 箱梁截面尺寸（单位：cm）

Figure 8. Box girder cross section （unit： cm）

下载: 全尺寸图片幻灯片

表 1 箱梁反对称畸变计算值

Table 1. Antisymmetrical distortional values

方法	I_ωd1/m⁶	I_R1/m²	ω_dD/m²	ω_dA/m²	β₁	γ_d1/（ × 10⁻¹⁰ rad）	B_d/（N·m²）	σ_dA/kPa	σ_dD/kPa
单箱单室箱梁畸变	12.1728	0.0040	2.5426	1.2075	0.4749	3.3961	2.6279	0.5213	1.0978
单箱双室箱梁反对称畸变	12.1728	0.0096	2.5426	1.2075	0.4749	1.7660	2.1110	0.2094	0.4409

下载: 导出CSV

| 显示表格

单箱单室箱梁增加一道腹板成为单箱双室箱梁后，σ_dA由0.5213 kPa变为0.2094 kPa，应力减小率为：（0.5213−0.2094）/ 0.5213 × 100%=59.83%，σ_dD的减小率也为59.83%. 因单室和双室箱梁反对称畸变的假定相同，角点应力比β₁数值不变，各角点的畸变扇性坐标数值不变. 由于中腹板增强了截面的横向抗弯刚度，箱梁的框架横向抗弯惯性矩从单室的0.0040增大到双室的0.0096.

算例箱梁正对称畸变计算值如表2所列. 单箱双室箱梁角点A的正对称畸变正应力为反对称畸变值的28.08%，角点D为26.76%. 若取的一半结构按照传统的单箱单室箱梁畸变方法计算角点畸变正应力，角点D的值为单箱双室箱梁反对称畸变值的1.97倍，为按照本文正对称畸变计算值的7.37倍.

表 2 箱梁正对称畸变计算值

Table 2. Positive-symmetrical distortional values

方法	角点应力比	γ_d/（ × 10⁻¹⁰ rad）	σ_dA/kPa	σ_dD/kPa
单箱双室箱梁正对称畸变	β₁ = 0.5000， β₂ = 0.6241	0.0160	0.05897	0.11795
单箱单室箱梁畸变	0.3229	3.7516	0.28055	0.86898

下载: 导出CSV

| 显示表格

最终单箱双室箱梁角点A、D的畸变正应力为箱梁正、反对称畸变计算结果的叠加，如表3. 并与有限元结果进行对比，有限元计算采用Shell-63单元建模分析. 从角点A、D的畸变正应力误差来看，本文方法解析解和有限元解最大误差的绝对值不超过8.71%，角点A的畸变正应力误差仅为1.73%，有限元解和解析解吻合良好.

表 3 箱梁角点畸变正应力

Table 3. Corner distortion normal stress of box girder

畸变正应力	单箱双室箱梁畸变解析解/kPa			有限元解 ②/kPa	误差（（①−②）/② × 100） /%
畸变正应力	反对称畸变	正对称畸变	最终结果 ①	有限元解 ②/kPa	误差（（①−②）/② × 100） /%
σ_dA	0.20940	0.05897	0.26837	0.26380	1.73
σ_dD	0.44090	0.11795	0.55885	0.61220	−8.71

下载: 导出CSV

| 显示表格

本文方法得到的双室箱梁和按单箱单室箱梁计算的角点A、D的应力值如表3和表1所示. 考虑箱梁的正对称畸变后，箱梁由单箱单室变成单箱双室时，角点A畸变正应力的减小率由59.83%变为48.52%，角点D畸变正应力的减小率由59.83%变为49.09%，如忽略正对称畸变的影响，畸变效应和有限元结果的误差将会增大. 双室箱梁的畸变正应力比单室箱梁的要小. 当箱梁横向宽度较大时，增设中腹板可有效减小箱梁的畸变效应.

为更好地比较两种截面形式箱梁的畸变效应差别. 单箱单室和单箱双室简支箱梁跨中截面的畸变角、角点畸变正应力的对比如图9、10所示. 由图9可知：单箱双室箱梁的反对称畸变角沿梁长的分布在畸变角数值的绝对值上小于单箱单室箱梁；中腹板对箱梁畸变的削弱非常明显，跨中截面畸变角迅速变小；在梁端一定区域内，双室箱梁的畸变角变化比单室的平稳，双室箱梁在此区域的反向变形小于单室箱梁，畸变角较早地衰减趋向于0，偏心竖向荷载引起的畸变较单箱单室箱梁的小，较好地反映了增加的箱室腹板对畸变的限制作用，与增加梁跨内横隔板效果相同.

图 9 畸变角沿梁长变化

Figure 9. Distortional angle changes of box girder

下载: 全尺寸图片幻灯片

图 10 角点A畸变正应力沿梁长变化

Figure 10. Changes of distortional normal stress of point A

下载: 全尺寸图片幻灯片

由图10可知：对箱梁畸变正应力沿梁长的分布进行分析，单室箱梁和双室箱梁角点A的畸变正应力沿梁长的分布有着明显的区别；双室箱梁角点A畸变正应力在数值的绝对值上明显小于单室箱梁，在跨中截面有最大值；双室箱梁角点A的畸变正应力向梁端衰减很快，而单室箱梁则衰减较慢. 从以上分析可以看出，双室箱梁畸变角、畸变正应力计算值都小于单室箱梁，中腹板对箱梁畸变的限制是非常明显的.

取中腹板厚度为0.10、0.15、0.20、0.25、0.30、0.35、0.40、0.45、0.50 m，其他条件皆不变，分析箱梁跨中截面反对称畸变角随中腹板厚度变化的规律. 中腹板厚度变化时，双室箱梁反对称畸变的畸变角沿梁长的变化情况如图11所示. 选取中腹板厚度为0.10、0.30、0.50 m的数据列出，0.10 m厚的板为薄板，0.30 m厚的板为薄板和厚板的界限，0.50 m厚的板为厚板.

图 11 中腹板厚度对箱梁畸变角的影响

Figure 11. Influence of mid-web thickness on distortional angle of box girder

下载: 全尺寸图片幻灯片

从图11可以看出：不同中腹板厚度的双室箱梁反对称畸变角沿梁长的变化趋势在箱梁跨中截面区域内基本相同，在箱梁梁端附近变化趋势有所不同；随着中腹板厚度的增加，在梁端附近，畸变角的变化逐渐平稳，双室箱梁在梁端附近畸变翘曲的程度较小；中腹板厚度为0.10 m的双室箱梁畸变角在梁端附近的反向变形比0.50 m板厚的要突出，薄壁箱梁的畸变翘曲程度比厚壁的要明显；随着板厚的增加，双室箱梁的畸变逐渐减小，仅在跨中一定长度范围内畸变较为明显，梁两端逐渐减弱，梁端变形程度较小的区域逐渐向跨内延伸；0.50 m板厚的双室箱梁梁端畸变较小的区域较0.10 m板厚的区域要长.

5. 结　论

1）在偏心竖向荷载作用下，单箱双室箱梁不仅存在反对称畸变，还存在正对称畸变. 正对称畸变正应力较小，本文算例中，最大只占到反对称畸变正应力的28.08%.

2）考虑了正对称畸变效应后，双室箱梁的畸变分析在理论上将更加完善. 通过数值计算显示，畸变正应力解析解和有限元解的误差减小，误差绝对值最大为8.71%，相互吻合更好.

3）当箱体较宽的单箱单室箱梁增设中间腹板成为单箱双室箱梁后，箱梁角点处的畸变正应力可减少到单室箱梁的49.09%. 为减小宽箱梁在偏心竖向荷载作用下的畸变，设置中腹板效果明显.

4）单箱双室简支箱梁的畸变比单箱单室简支箱梁的要小，变形主要在跨中一定的区域内，梁端附近的区域反向变形不如单箱单室的明显. 中腹板厚度的变化可使双室箱梁的畸变发生较明显的改变，厚度较小时畸变较为明显，厚度增大时畸变逐渐减弱.

5）采用两个参数β₁、β₂描述正对称畸变时，单箱双室箱梁各板件上的畸变正应力分布比一个参数的合理. 采用一个参数的箱梁畸变理论计算的正对称畸变效应，箱梁角点畸变正应力最大可为本文方法的7.37倍.

图 1 一阶逻辑公式的双向图表示

Figure 1. Bidirectional graph representation of first-order logical formula

下载: 全尺寸图片幻灯片

图 2 基于图神经网络的前提选择模型

Figure 2. Premise selection model based ongraph neural network

下载: 全尺寸图片幻灯片

表 1 MPTP2078问题库描述

Table 1. Description of MPTP2078 benchmark 条

名称	公式	结论	最小前提	最大前提	平均前提
数量	4 564	2 078	10	4 563	1 876

下载: 导出CSV

表 2 数据集划分

Table 2. Division of datasets 个

样本	训练集	验证集	测试集
正	27663	3417	3432
负	27556	3485	3471
总样本	55219	6902	6903

下载: 导出CSV

表 3 参数设置

Table 3. Setting of parameters

参数	设置
节点向量维度 ${d}_{{h}_{v}}$	64
边向量维度 ${d}_{{h}_{e}}$	32
迭代次数 K/次	1
学习率	0.0010
学习率衰减系数	0.1
学习率衰减步长	50
轮次/轮	100
权重衰减	0.0001
批量大小/个	8

下载: 导出CSV

表 4 数据集上的对比实验结果

Table 4. Comparision of experimental results on datasets

方法	准确率	精确率	召回率	F₁
GCN^[18]	0.8625	0.8669	0.8547	0.8608
GAT^[19]	0.858 0	0.862 9	0.851 8	0.857 3
GraphSAGE^[27]	0.8615	0.8686	0.8501	0.8592
SGC^[28]	0.8557	0.8579	0.8506	0.8543
Chebyshev^[29]	0.8608	0.8660	0.8518	0.8588
EW-GNN	0.8724	0.8701	0.8686	0.8641

下载: 导出CSV

参考文献(29)

[1]	KERN C, GREENSTREET M R. Formal verification in hardware design: a survey[J]. ACM Transactions on Design Automation of Electronic Systems (TODAES), 1999, 4(2): 123-193. doi: 10.1145/307988.307989
[2]	KLEIN G, ELPHINSTONE K, HEISER G, et al. seL4: Formal verification of an OS kernel[C]//Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles. Big Sky: ACM, 2009: 207-220.
[3]	LEROY X. Formal verification of a realistic compiler[J]. Communications of the ACM, 2009, 52(7): 107-115. doi: 10.1145/1538788.1538814
[4]	KOVÁCS L, VORONKO A. First-order theorem proving and vampire[C]//25th International Conference on Computer Aided Verification. Saint Petersburg: [s.n.], 2013: 1-35.
[5]	SCHULZ S. E – a brainiac theorem prover[J]. Ai Communications, 2002, 15(2/3): 111-126.
[6]	SUTCLIFFE G. The TPTP problem library and associated infrastructure[J]. Journal of Automated Reasoning, 2017, 59(4): 483-502. doi: 10.1007/s10817-017-9407-7
[7]	KALISZYK C, URBAN J. MizAR 40 for mizar 40[J]. Journal of Automated Reasoning, 2015, 55(3): 245-256. doi: 10.1007/s10817-015-9330-8
[8]	MCCUNE W W. Otter 3.0 reference manual and guide[R]. Chicago: Argonne National Lab., 1994.
[9]	MENG J, PAULSON L C. Lightweight relevance filtering for machine-generated resolution problems[J]. Journal of Applied Logic, 2009, 7(1): 41-57. doi: 10.1016/j.jal.2007.07.004
[10]	HODER K, VORONKOV A. Sine qua non for large theory reasoning[C]//23th International Conference on Automated Deduction. Wroclaw: [s.n.], 2011: 299-314.
[11]	ALAMA J, HESKES T, KÜHLWEIN D, et al. Premise selection for mathematics by corpus analysis and kernel methods[J]. Journal of Automated Reasoning, 2014, 52(2): 191-213. doi: 10.1007/s10817-013-9286-5
[12]	KALISZYK C, URBAN J, VYSKOČIL J. Efficient semantic features for automated reasoning over large theories[C]//Proceedings of the 24th International Conference on Artificial Intelligence. [S.l.]: AAAI Press, 2015: 3084-3090.
[13]	PIOTROWSKI B, URBAN J. ATPboost: learning premise selection in binary setting with ATP feedback[C]//International Joint Conference on Automated Reasoning. Cham: Springer, 2018: 566-574.
[14]	ALEMI A A, CHOLLET F, EEN N, et al. DeepMath-deep sequence models for premise selection[C]// Proceedings of the 30th International Conference on Neural Information Processing Systems. Barcelona: Curran Associates Inc., 2016: 2243-2251.
[15]	WANG M, TANG Y, WANG J, et al. Premise selection for theorem proving by deep graph embedding[C]//Proceedings of the 31st International Conference on Neural Information Processing Systems. Long Beach: Curran Associates Inc., 2017: 2783-2793.
[16]	CROUSE M, ABDELAZIZ I, CORNELIO C, et al. Improving graph neural network representations of logical formulae with subgraph pooling[EB/OL]. (2019-11-15). https://arxiv.org/abs/1911.06904.
[17]	PALIWAL A, LOOS S, RABE M, et al. Graph representations for higher-order logic and theorem proving[C]//34th Proceedings of the AAAI Conference on Artificial Intelligence. Palo Alto: AAAI Press, 2020: 2967-2974.
[18]	KIPF T N, WELLING M. Semi-supervised classification with graph convolutional networks[DB/OL]. (2016-09-09). https://doi.org/10.48550/arXiv.1609.02907.
[19]	VELIČKOVIĆ P, CUCURULL G, CASANOVA A, et al. Graph attention networks[DB/OL]. (2017-10-30). https://doi.org/10.48550/arXiv.1710.10903.
[20]	ROBINSON A J, VORONKOV A. Handbook of automated reasoning[M]. [S.l.]: Elsevier, 2001.
[21]	Rudnicki P. An overview of the Mizar project[C]//Proceedings of the 1992 Workshop on Types for Proofs and Programs. [S.l.]: Chalmers University of Technology, 1992: 311-330.
[22]	JAKUBŮVJ, URBAN J. ENIGMA: efficient learning-based inference guiding machine[C]//International Conference on Intelligent Computer Mathematics. Cham: Springer, 2017: 292-302.
[23]	COVER T, HART P. Nearest neighbor pattern classification[J]. IEEE Transactions on Information Theory, 1967, 13(1): 21-27.
[24]	PASZKE A, GROSS S, MASSA F, et al. PyTorch: an imperative style, high-performance deep learning library[DB/OL]. (2019-12-03). https://arxiv.org/abs/1912.01703
[25]	FEY M, LENSSEN J E. Fast graph representation learning with PyTorch geometric[DB/OL]. (2019-03-06). https://arxiv.org/abs/1903.02428
[26]	KINGMA D P, BA J. Adam: a method for stochastic optimization[DB/OL]. (2014-12-22). https://arxiv.org/abs/1412.6980.
[27]	HAMILTON W L, YING R, LESKOVEC J. Inductive representation learning on large graphs[C]//Proceedings of the 31st International Conference on Neural Information Processing Systems. Long Beach: [s.n.], 2017: 1025-1035.
[28]	WU F L, SOUZA A H, ZHANG T Y, et al. Simplifying graph convolutional networks[C]// International Conference on Machine Learning. [S.l.]: PMLR, 2019: 6861-6871.
[29]	DEFFERRARD M, BRESSON X, VANDERGHEYNST P. Convolutional neural networks on graphs with fast localized spectral filtering[C]//Proceedings of the 30th International Conference on Neural Information Processing Systems. Barcelona: [s.n.], 2016: 3844-3852.

施引文献

期刊类型引用(3)

1.	马雪，何星星，兰咏琪，李莹芳. 一阶逻辑中基于treelet图神经网络的前提选择. 计算机工程与科学. 2024(02): 374-380 . 百度学术
2.	曹锋，谢燏，易见兵，李俊. 矛盾体分离单元结果演绎方法及应用. 计算机工程与科学. 2024(12): 2252-2260 . 百度学术
3.	刘清华，李瑞杰，朱绪胜，陈代鑫. 基于符号权重的一阶逻辑前提选择方法. 西南交通大学学报. 2023(03): 704-710 . 本站查看