Contradiction separation (CS) and its first-order version S-CS are multi-clause inference schemes for clausal refutation. They isolate a standard contradiction core within a clause set and derive a propagated clause from the remaining literals. This paper develops structural characterizations of non-unit standard contradictions that make such cores explicit and easier to identify. In propositional logic, we introduce a canonical dual-line family and prove that every instance is a standard contradiction. We study admissible literal extensions, define ladder structures as maximal dual-line extensions, and present a regular triple-line family with constructive generation schemes. We also analyze how dual-line cores compose via clause connections and give sufficient conditions under which the composed clause set remains a standard contradiction. In first-order logic, we exhibit clause families that are not standard contradictions syntactically but become standard contradictions after suitable instantiation and controlled clause reuse.

Premise selection effectively addresses large-theory theorem-proving challenges, where Graph Neural Networks (GNNs) and their variants are commonly used methods. Conversely, optimizing a graph representation of formulas in first-order logic is rarely addressed, particularly in terms of simplification and the logical properties preserved during the embedding process. This paper proposes an attention term-walk based GNN with a simplified graph representation (ATWGNNS) for premise selection. First, a simplified formula graph representation method is introduced, where repeated quantifiers in the formula graph are eliminated. Next, we present methods for measuring the similarity of formulas and graphs. It is demonstrated that the similarity of graphs without repeated quantifiers is greater than that of other graphs that retain the original quantifiers. Furthermore, the higher the similarity of the logical formulas, the greater the similarity of the corresponding graphs. This confirms the interpretability of the graph representation method. Finally, a term-walk based GNN with an attention mechanism is proposed to retain task-relevant structural information in simplified formula graphs after removing repeated quantifiers. The experimental results demonstrate that the model developed using the proposed method outperforms state-of-the-art models in premise selection.

Automated deduction based on contradiction separation extends the binary resolution principle, offering a novel approach to deductive inference rules. Constructing standard contradictions is essential for its efficiency. This paper systematically investigates two new types of standard contradictions in propositional and first-order logic, enriching the library of standard contradictions and enhancing its effectiveness. First, we define two types of standard contradictions: sign-boundary contradictions and diagonal vacancy-type contradictions. Next, we propose the corresponding construction methods and present their properties related to contradiction composition and literal addition. Furthermore, we explore the transformations between these two types of contradictions and analyze the conditions necessary to construct standard contradictions. Finally, we extend these findings to first-order logic, demonstrating their applicability in more complex logical systems.

Premise selection for first-order automated theorem proving is a challenging task, as a prover must identify a small set of truly relevant premises from thousands of candidates in large formal knowledge bases. Although graph neural network–based methods have achieved promising results, most existing approaches treat logical formulas as homogeneous graphs and fail to explicitly model the semantic hierarchy inherent in first-order logic.In this paper, we propose HLACGNN, a Hierarchical Logic-aware Cross-Graph Neural Network for premise selection. HLACGNN explicitly decomposes first-order logic formulas into semantically meaningful units and represents them as structured semantic subgraphs within formula graphs. Based on this semantic abstraction, HLACGNN enables structured interaction between conjecture and premise graphs, allowing premise relevance to be assessed through fine-grained alignment of logically salient substructures rather than global graph similarity alone. Furthermore, a hierarchical attention-based aggregation mechanism is introduced to preserve the semantic organization of logical formulas when constructing graph-level representations. Beyond performance gains, the learned attention distributions over semantic units exhibit interpretable patterns that align with established domain knowledge in first-order logic.Experiments on the MPTP2078 benchmark, including both original first-order formulas and their CNF-transformed counterparts, demonstrate that HLACGNN consistently outperforms state-of-the-art graph-based premise selection models, achieving a performance gain of close to 2\% over the strongest competing baselines. Notably, the performance improvements are more pronounced on original first-order formulas, highlighting the advantage of explicitly modeling semantic hierarchy, which is partially diminished in CNF representations due to structural flattening. When integrated into the E theorem prover under a fixed time budget, HLACGNN improves proof success rates by 19\%, demonstrating its effectiveness for large-theory automated reasoning.

Trustworthy AI requires reasoning systems that are not only powerful but also transparent and reliable. Automated Theorem Proving (ATP) is central to formal reasoning, yet classical binary resolution remains limited, as each step involves only two clauses and eliminates at most two literals. To overcome this bottleneck, the concept of standard contradiction and the theory of contradiction-separation-based deduction were introduced in 2018. This paper advances that framework by focusing on the systematic construction of standard contradictions. Specially, this study investigates construction methods for two principal forms of standard contradiction: the maximum triangular standard contradiction and the triangular-type standard contradiction. Building on these structures, we propose a procedure for determining the satisfiability and unsatisfiability of clause sets via maximum standard contradiction. Furthermore, we derive formulas for computing the number of standard sub-contradictions embedded within both the maximum triangular standard contradiction and the triangular-type standard contradiction. The results presented herein furnish the methodological basis for advancing contradiction-separation-based dynamic multi-clause automated deduction, thereby extending the expressive and deductive capabilities of automated reasoning systems beyond the classical binary paradigm.

AIMS:Among the novel metrics derived from continuous glucose monitoring (CGM), time in tight range (TITR) has gained increasing attention. Our study aimed to investigate the relationship between 1,5-anhydroglucitol (1,5-AG) and TITR in patients with type 2 diabetes. MATERIALS AND METHODS:This cross-sectional study included 1531 moderately controlled patients with type 2 diabetes on a stable treatment regimen. TITR and time in range (TIR) were measured with CGM. Spearman correlation analysis was used to assess the relationship between serum 1,5-AG and TITR, and the predictive efficacy of serum 1,5-AG for identifying TITR > 50% was evaluated by the receiver operating characteristic curves. RESULTS:The median levels of serum 1,5-AG and glycated haemoglobin A1c (HbA1c) in the total population were 7.4 (4.4, 12.1) μg/mL and 7.0% (6.4%, 7.5%), respectively. The median TITR was 52.0% (32.0%, 69.0%). Spearman correlation analysis showed that serum 1,5-AG was positively correlated with TITR (p < 0.001). The optimal serum 1,5-AG cut-off for TITR >50% was 8.0 μg/mL, with an area under the curve (AUC) of 0.693 (0.667, 0.719). Serum 1,5-AG combined with fasting glucose or 2-hour postprandial glucose further improved the predictive power for identifying TITR > 50% (both p < 0.001). Across all subgroups, serum 1,5-AG showed acceptable predictive accuracy for TITR > 50% (AUCs around 0.700). CONCLUSIONS:Serum 1,5-AG was significantly correlated with TITR in patients with type 2 diabetes, with 8.0 μg/mL emerging as a potential cut-off for identifying TITR > 50%.

Automated deduction seeks to enable machines to reason with mathematical precision and logical completeness. Classical resolution-based systems, such as Prover9, E, and Vampire, rely on binary inference, which inherently limits multi-clause synergy during proof search. The Contradiction Separation Extension (CSE) framework, introduced by Xu et al. (2018), overcame this theoretical limitation by extending deduction beyond binary inference. However, the original work did not specify how contradictions are algorithmically constructed and extended in practice. This paper presents the Standard Extension algorithm, the first explicit procedural realization of contradiction separation reasoning. The proposed method dynamically constructs contradictions through complementary literal extension, thereby operationalizing the CSE theory within a unified algorithm for satisfiability and unsatisfiability checking. The algorithm's soundness and completeness are formally proven, and its effectiveness is supported indirectly through the performance of CSE-based systems, including CSE, CSE-E, CSI-E, and CSI-Enig in major automated reasoning competitions (CASC) in the last few years. These results confirm that the Standard Extension mechanism constitutes a robust and practically validated foundation for dynamic, multi-clause automated deduction.

Automated deduction lies at the core of Artificial Intelligence (AI), underpinning theorem proving, formal verification, and logical reasoning. Despite decades of progress, reconciling deductive completeness with computational efficiency remains an enduring challenge. Traditional reasoning calculi, grounded in binary resolution, restrict inference to pairwise clause interactions and thereby limit deductive synergy among multiple clauses. The Contradiction Separation Extension (CSE) framework, introduced in 2018, proposed a dynamic multi-clause reasoning theory that redefined logical inference as a process of contradiction separation rather than sequential resolution. While that work established the theoretical foundation, its algorithmic realization remained unformalized and unpublished. This work presents the Extended Triangular Method (ETM), a generalized contradiction-construction algorithm that formalizes and extends the internal mechanisms of contradiction separation. The ETM unifies multiple contradiction-building strategies, including the earlier Standard Extension method, within a triangular geometric framework that supports flexible clause interaction and dynamic synergy. ETM serves as the algorithmic core of several high-performance theorem provers, CSE, CSE-E, CSI-E, and CSI-Enig, whose competitive results in standard first-order benchmarks (TPTP problem sets and CASC 2018-2015) empirically validate the effectiveness and generality of the proposed approach. By bridging theoretical abstraction and operational implementation, ETM advances the contradiction separation paradigm into a generalized, scalable, and practically competitive model for automated reasoning, offering new directions for future research in logical inference and theorem proving.

Multi-instance learning (MIL) is a widely applied technique in practical applications that involve complex data structures. MIL can be broadly categorized into two types: traditional methods and those based on deep learning. These approaches have yielded significant results, especially regarding their problem-solving strategies and experiment validation, providing valuable insights for researchers in the MIL field. However, considerable knowledge is often trapped within the algorithm, leading to subsequent MIL algorithms that rely solely on the model's data fitting to predict unlabeled samples. This results in a significant loss of knowledge and impedes the development of more powerful models. In this article, we propose a novel data-driven knowledge fusion for deep MIL (DKMIL) algorithm. DKMIL adopts a completely different idea from existing deep MIL methods by analyzing the decision-making of key samples in the dataset (referred to as the data-driven) and using the knowledge fusion module designed to extract valuable information from these samples to assist the model's learning. In other words, this module serves as a new interface between data and the model, providing strong scalability and enabling prior knowledge from existing algorithms to enhance the model's learning ability. Furthermore, to adapt the downstream modules of the model to more knowledge-enriched features extracted from the data-driven knowledge fusion (DDKF) module, we propose a two-level attention (TLA) module that gradually learns shallow- and deep-level features of the samples to achieve more effective classification. We will prove the scalability of the knowledge fusion module and verify the efficiency of the proposed architecture by conducting experiments on 62 datasets across five categories.

The search space for automatic theorem proving typically experiences exponential growth when attempting to prove a conclusion with numerous axioms. Premise selection presents a novel approach to tackle this challenge. However, one major obstacle lies in enhancing the presentation of logical formula graphs and graph neural network models in existing premise selection methods to preserve potential information from the logical formulas effectively. This study proposes a novel simplified graph representation of logical formulas by eliminating repeated quantifiers, along with a new term-walk graph neural network model incorporating an attention mechanism and attention pooling (ASTGNNS). This model aims to preserve syntax and semantic information of logical formulas, particularly regarding the order of symbols and the scope of quantifiers in logical formulas, thereby improving classification accuracy in premise selection problems. Specifically, we first transform first-order logical conjectures and premise formulas into simplified logical formula graphs by removing repeated quantifiers. Next, we introduce a method based on a common path kernel function to measure graph similarity and validate the interpretability of our simplified logical formula graphs method. Then, an attention mechanism is employed to assign weights to term-walk feature information of nodes for updating node feature representations; meanwhile, attention pooling is utilized for selecting nodes that significantly contribute towards generating the final formula graph vector. Finally, combining the premise graph vector and conjecture graph vector forms a binary classifier for classification purposes. Experimental results demonstrate that our proposed method achieves an accuracy rate of 88.77% on the MPTP dataset and 85.17% on the CNF dataset, outperforming the state-of-the-art premise selection method.

Multi-criteria decision-making (MCDM) is a popular branch of decision theory in which many methods have been proposed to solve MCDM real-world problems. However, in spite of the multiple methods, it is common that different of them provide the same solutions. Therefore, this paper analyzes the causes of the same solutions from different MCDM methods, studies why different normalization methods can achieve the same solutions in MCDM methods through the theory of MCDM methods, and discusses the relationship between different MCDM methods by category. To achieve such goals, MCDM methods are classified into three categories according to their ranking methods. Some traditional MCDM methods are then extended by considering general normalization methods and distance measures. Finally, the characteristics of various MCDM methods are discussed by category and their evaluation indexes are also compared. The comparison results are represented by tables and flowchart models. The relationship between different categories of MCDM methods is shown through the comparison of the evaluation indexes. The aim of the proposed method is not to replace existing MCDM methods, but to fill some present research gaps about MCDM methods.

In this article, the authors propose a new educational grading system based on fuzzy techniques, which includes five interrelated modules. Through an example to illustrate the process of the proposed fuzzy educational grading system, we find that the proposed system meets the basic requirements of the educational grading system and can overcome the limitations of existing fuzzy educational grading systems. By comparing the proposed fuzzy educational grading system with traditional methods, we find that the proposed evaluation system can more objectively and intelligently evaluate students’ answer sheets. The aim of the proposed method is not to replace the existing fuzzy educational grading systems, but to enrich the present systems for students’ learning achievement evaluation.

This paper presents an improved method for estimating the similarity between LR-type fuzzy numbers. By considering different left and right shape functions, we can conveniently compute the similarity between trapezoidal fuzzy numbers, Gaussian fuzzy numbers and normal fuzzy numbers. An algorithm for computing the proposed similarity measure between LR-type fuzzy numbers and a numerical method for approximating it are provided. Some of its properties are also examined. The performance of the proposed method is compared with some existing similarity measures through using different sets of LR-type fuzzy numbers. It is shown that the similarity between LR-type fuzzy numbers with parameters from any real number belonged to the real number set R is considered in the proposed method. The given similarity measure is scale-invariant and takes into account the shape of LR-type fuzzy numbers, which can overcome the shortcomings of existing methods.

In many real-world decision-making tasks, multi-agent need to learn collaboration in a high-dimensional complex action space, rather than just a single discrete action space. Recently, value decomposition learning methods such as QMIX have emerged as a promising approaches for collaborative multi-agent tasks. However, most of the value decomposition algorithms can only be used in discrete action space, which would limit their practicability. To address the limitation, we propose a novel algorithm called Multi-Agent Sequential Q-Networks (MASQN), which can be applied to the multi-agent domains with continuous, multidiscrete or hybrid action spaces. The proposed algorithm is based on the structure of centralized training with decentralized execution (CTDE). The decentralized actors ensure adaptability to different action spaces by utilizing action space discretization and sequential models, and the centralized critic utilizes the value decomposition architecture to guide effective updates of the policy parameters for each agent. We also give the convergence of joint policy from the perspective of policy iteration, by combining it with the CTDE structure and the constraint of the Individual Global Max (IGM) condition. Finally, we evaluate the MASQN algorithm on two benchmark environments: MAMuJoCo and Hybrid Predator-Prey. The empirical results show that MASQN out performs the state-of-the-art performance on three different action spaces.

The search space of automatic theorem proving typically experiences exponential growth when attempting to prove a conclusion with numerous axioms. Premise selection offers a novel approach to addressing this challenge. However, one major obstacle lies in the need for enhancing the logical formula graph presentation and the graph neural network model in existing premise selection methods to effectively capture potential information from the logical formulas. In this study, we propose a novel simplified graph representation of logical formulas by eliminating repeated quantifiers, along with a new term-walk graph neural network model incorporating an attention mechanism and attention pooling (ASTGNNS). This model aims to preserve both syntax and semantic information of logical formulas, thereby improving classification accuracy in premise selection problems. Specifically, we first transform first-order logical conjectures and premise formulas into simplified logical formula graphs by removing repeated quantifiers. Next, we introduce a method based on common path kernel function to measure graph similarity and justify the rationality of simplified logical formula graphs method. Then, an attention mechanism is employed to assign weights to term-walk feature information of nodes for updating node feature representations; meanwhile, attention pooling is utilized for selecting nodes that contribute significantly towards generating the final formula graph vector. Finally, combining the premise graph vector and conjecture graph vector forms a binary classifier for classification purposes. Experimental results demonstrate that our proposed method achieves an accuracy rate of 88.77% on the MPTP dataset and 85.17% on the CNF dataset, outperforming state-of-the-art premise selection methods.

Supplementary Figure S3. In vivo imaging of MMP activity and tumor growth.

人工智能是用计算机来模拟人的某些思维过程和智能行为的学科.自动推理中的归结原理是一种简洁、可靠且完备的推理规则.矛盾体的动态多子句协同演绎理论不仅是归结原理的重要延拓,而且具有较高的推理演绎效率.由于矛盾体的结构复杂、生成策略较少,因此在矛盾体的动态演绎可靠性和完备性的基础上,提出复合2个或多个矛盾体的部分子句的不同策略,为矛盾体的构造提供了一种有效的方法.

Supplementary Figure S4. The HMGB1-IL6-STAT3-miR-21 axis promotes HCC tumor progression.

Supplementary Tables S1-S2. Primer pairs for qRT-PCR (S1); Oligonucleotides used for cloning RECK/TIMP3 3'UTR to pMIR-REPORT (S2).

Interval-valued fuzzy logical connectives are extensions of fuzzy logical connectives to the interval-valued framework. The extensions require linear orders to define the monotonicity between intervals. As a significant linear order, the admissible order is introduced to compare any interval in interval-valued fuzzy logic. In this work, we examine several widely-used interval-valued fuzzy logical connectives with respect to admissible orders. We are concerned with interval-valued fuzzy negations, automorphisms, fuzzy implications and aggregation functions with respect to K-alpha,K- beta orders and arbitrary intervals on L([0, 1]). We also make a discussion of width-preserving interval-valued fuzzy equivalence functions and dissimilarity functions with respect to arbitrary admissible orders and the intervals with the same width on L([0, 1]). Then we bring some approaches to constructing the proposed interval-valued fuzzy logical connectives with respect to admissible orders. The introduced interval-valued fuzzy logical connectives with respect to admissible orders may have a deep impact on some fields exploiting fuzzy methods dealing with intervals.