Trustworthy AI requires reasoning systems that are both powerful and transparent. Automated Reasoning (AR) is central to formal reasoning, yet classical binary resolution is limited: each step handles only two clauses and removes at most two literals. To move beyond this bottleneck, the concepts of standard contradiction and contradiction-separation-based deduction were introduced in 2018. This paper extends that framework by systematically constructing and applying standard contradictions for multi-clause deduction and automated theorem generation. We focus on two key forms—the maximum triangular and triangular-type standard contradictions—and present methods for building them. Using these structures, we develop a procedure to test the satisfiability of clause sets and derive formulas to count the sub-contradictions they contain. These results establish a foundation for dynamic multi-clause automated deduction and theorem generation, expanding the expressive and deductive reach of reasoning systems beyond the classical binary paradigm.

Theorem machine proving holds a fundamental, historical, and interdisciplinary position in the field of artificial intelligence. It is not only one of the core directions of early AI research but also serves as a crucial technical support for modern intelligent systems to achieve logical reasoning and symbolic processing capabilities. The automatic reasoning method based on resolution is a crucial approach for theorem machine proving, and it has been widely applied in multiple domains. To further enhance the efficiency of resolution reasoning, this paper focuses on the research of inclusion relationships between clause sets in propositional logic, derives some properties of inclusion relationships, and illustrates these properties through examples. These conclusions provide certain theoretical support for further establishing corresponding resolution reasoning methods based on inclusion relationships.

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.

时序逻辑是研究状态随时间变化系统的逻辑特性,在软硬件验证中有着广泛应用,是模型检测的基础.基于对时间模型的不同描述以及为了处理更加复杂的计算特征,衍生出各种时序逻辑,具有不同的表达能力,正确理解其表达能力对于系统模型的形式化规约尤为重要.首先,介绍基于离散时间模型的线性时序逻辑LTL、计算树逻辑CTL和CTL*,以及基于连续时间模型的区间时序逻辑ITL和投影时序逻辑PTL,对它们的表达能力及区别进行了详细阐述;然后,概述为了描述随机、实时、混成、开放系统中的复杂行为而提出的不同时序逻辑,指出它们的特点及适用范围;最后,对时序逻辑的未来研究方向进行展望.

Non-repudiation protocols are aimed at exchanging digital messages and irrefutable receipts between two mistrusting parties over the Internet, which form the cornerstones of modern secure network transactions. Timeliness is a key security property of non-repudiation protocols, which ensures that protocol agents can terminate their execution within a finite time, and guarantees the satisfaction of time-constraint among protocol events. A number of analysis methods have been proposed, but most of them cannot explicitly express the time factor which plays an important role in protocols. In order to address the challenge of analyzing timeliness, this paper extends the logic of events theory (LoET) and proposes a novel formal logic. By explicitly introducing the time factor into predicate formulas, the new logic can model actions, knowledge, and process states of each agent at different time points, thus enhancing its ability of time description. The formal semantics of new logic is given to avoid ambiguity of logic language and guarantee the soundness of new logic. A typical non-repudiation protocol is analyzed with new logic, and the timeliness flaw is discovered. The proposed logic overcomes the limitations of LoET in terms of time description and effectively addresses the issue of the inability to analyze timeliness.

The increasing commercialization and massive deployment of radio frequency identification(RFID)systems has raised many security related issues which in return evokes the need of security protocols.Lo-gic of events theory(LoET)is a formal method for con-structing and reasoning about distributed systems and protocols that involve concepts of security.We propose fresh ciphertext and ciphertext release lemmas to extend LoET for analyzing and proving the security of authentic-ation protocols that use symmetric key cryptography more than just digital signature.Based on the extended LoET we formally analyze and prove the authentication property of RCIA protocol,which provides mutual au-thentication between Tag and Reader in RFID system.Our proof approach based on extended LoET could be ap-plied to the design and analysis of such ultralightweight RFID mutual authentication protocols.

自动推理是人工智能领域研究的核心问题之一.由于在基于归结的自动推理过程中会产生大量的冗余文字和冗余子句,进而影响归结自动推理的效率,因此消除子句集中的冗余文字和冗余子句具有重要的意义.在命题逻辑中,依据必需文字、有用文字、无用文字的相关概念和性质,针对部分三元子句集,分类给出这些三元子句集中冗余文字的判别方法,并通过具体实例对这些判别方法进行说明.

针对现有学习子句评估策略的单一性,提出一种基于学习子句参与冲突分析次数的评估策略,并将该策略分别与经典的文字块距离评估策略和活跃值评估策略结合,形成两个动态学习子句评估策略.基于2018年SAT国际竞赛部分基准实例,将动态评估策略与原评估策略进行参数适应性对比实验,并通过2018和2017年的基准实例进行评估.结果 表明动态评估策略能更好地评估学习子句的质量,由此生成的求解器在求解数量和速度方面表现出较好的求解性能.

With the increasing sizes of models and datasets, it has become a common practice to split machine learning jobs as multiple tasks. However, stragglers are inevitable when running a job on multiple servers. Compared to replicating each task on multiple servers, running coded tasks can tolerate the same number of stragglers with much fewer servers. However, additional results of tasks running on stragglers are typically disregarded in existing schemes of coded computing, incurring a waste of the resources on such servers. In this paper, we leverage the results of partially finished tasks. In existing designs that utilize partially finished tasks, they have only considered servers with homogeneous performance. However, in a typical distributed infrastructure, e.g., a cloud, servers with heterogeneous configurations are common. Therefore, we propose Spinner which can efficiently utilize the results of partially finished tasks even on heterogeneous servers. Spinner works with existing coding schemes for matrix multiplication, a fundamental operation in various machine learning algorithms, and can efficiently assign the workload based on the performance of the corresponding server. Furthermore, Spinner can equivalently adapt the coding scheme for heterogeneous servers, aligned with the expected workload assigned to each server, and thus save the complexity of decoding. Combining the two strategies together, we demonstrate in our experiments that Spinner can improve the time of matrix multiplication by up to 84.0% and thus improve the time of linear regression by 40.7%.

Matrix multiplication is a fundamental operation in various machine learning algorithms. With the size of the dataset increasing rapidly, it is now a common practice to compute the large-scale matrix multiplication on multiple servers, with each server running a task that multiplies submatrices of input matrices. As straggling servers are inevitable in a distributed infrastructure, various coding schemes, which deploy coded tasks encoded from input matrices, have been proposed. The overall result can then be decoded from a subset of such coded tasks. However, as resources are shared with other jobs in a distributed infrastructure and their performance can change dynamically, the optimal way to encode the input matrices may also change with time. So far, existing coding schemes for the matrix multiplication all require splitting the input matrices and encoding them in advance, and cannot change the coding schemes or adjust their parameters after encoding. In this paper, we propose a framework that can change the coding schemes and their parameters, by only locally re-encoding each task on each server. We demonstrate that the original tasks can be re-encoded into new tasks only incurring marginal overhead.

Nowadays, more and more new cryptographic protocols are emerging, and the security analysis of emerging cryptographic protocols is increasingly important. The logic of events is an axiomatic method based on theorem proving, designed around message automation with actions for possible protocol steps; it figured out types of information transmitted in the protocols and also presented novel proof rules and mechanism. However, with the emergence of various cryptographic protocols, the logic of events lacks corresponding axioms and rules in the process of proving certain cryptographic protocols, so it needs a further extension. Based on the logical framework of protocol composition logic, this paper presents a refined theory of the logic of events called LoET-E, in which the novel rules about the freshness of nonces, the event attributes of messages, and the states of the predicate is presented; the concepts of Fresh, Gen and FirstSend is introduced; and the definition of has and the honesty axiom of LoET is extended. The refined theory can guarantee the correctness, integrity, and validity of the original axioms, ensure the consistency of event classes and basic sequences in the proof process, reduce the complexity and redundancy in the protocol analysis process, and most importantly, extend the provable range of cryptographic protocols.

Ultralightweight mutual authentication protocols (UMAP) of Radio frequency identification (RFID) systems have attracted much attention from researchers. Many studies reveal that most of UMAP suffer malicious attack. To improve security of UMAP, formal analysis is performed with Simple promela interpreter (SPIN). Two typical UMAPs, which are RCIA and RAPP, are selected as our case study. A protocol abstract modeling method is presented to make UMAP can be formalized simply. Using SPIN, verification results show that RCIA and RAPP are both vulnerable against desynchronization attack. A Generalized model of UMAP (G-UMAP) and a general patching scheme are presented for resisting the attack. To validate the patching scheme, formal verification is then performed for the improved protocol. SPIN verification shows that the improved RCIA and RAPP both gain higher security. The above proposed modeling method has great significance for similar UMAP analyzing, and the proposed patching scheme is proved to be practical and reliable.

无线Mesh网络是一种新型的宽带无线网络结构,融合无线局域网与点对点模式两者的优势,是无线网络研究的热点之一.基于事件逻辑理论,结合事件结构、事件类、公理簇以及随机数引理,提出置换规则保证用户交互信息在性质置换过程中的等价转换.通过事件逻辑构建客户端与LTCA认证协议的基本序列,对协议交互动作进行形式化描述并证明协议强认证性质.在合理假设下,无线Mesh网络客户端与LTCA间认证协议的安全性得证,研究表明事件逻辑理论不仅可以论证无线网络协议的安全属性,还能对安全协议不同身份主体间的认证性进行证明.通过流程图简化协议形式化证明步骤,阐述事件逻辑理论证明协议安全属性过程,比较分析事件逻辑理论与其他逻辑推理方法,表明事件逻辑理论具有通用性.

RFID three-party authentication protocol based on NTRU cryptosystem is a type of multi-entities authentication protocol. Unlike other RFID mutual authentication protocols, this protocol realizes mutual authentication of Server to Reader, and Server to Tag. Model checking is a formal method to check the correctness specifications hold in each state on concurrent and distributed systems, which can be used to verify the security of network protocol. A multi-channels constructing method is proposed to build this protocol model for formal analysis, then authentication property of the protocol is verified by model checker SPIN. Formal verification result reveals that an attack exists in this protocol, hence the protocol cannot guarantee the security of the three-party authentication protocol. The modeling method proposed above has great significance on security analysis for such three-party authentication protocols.

Contradiction separation based dynamic automated deduction is a novel development of the standard static (i.e., fixed) binary resolution into a dynamic multi-clause synergized contradiction separation based inference rule. In this paper, we consider some distinctive features/advantages of this novel automated deduction mechanism, including multi-clause involvement, dynamic deduction, synergized deduction, robustness, exchangeability, controllability, scaling, repeatability, integrity and flexibility, along with some illustrative examples.

Due to the need of the logical foundation for uncertain information processing, development of efficient automated reasoning system based on non-classical logics is always an active research area. The present paper focuses on the resolution-based automated reasoning theory in a many-valued logic with truth-values defined in a lattice-ordered many-valued algebraic structure - lattice implication algebras (LIA). Specifically, as a continuation and extension of the established work on binary resolution at a certain truth-value level α (called α -resolution), a non-clausal multi-ary α -generalized resolution calculus is introduced for a lattice-valued propositional logic LP(X) based on LIA, which is essentially a non-clausal generalized resolution avoiding reduction to normal clausal form. The new resolution calculus in LP(X) is then proved to be sound and complete. The concepts and theoretical results are further extended and established in the corresponding lattice-valued first-order logic LF(X) based on LIA.

The near field communication (NFC) is widely used on mobile devices and make it possible to take advantage of NFC system to complete mobile payment. But with the development of NFC, its problem are increasingly exposed, especially the security and privacy of authentication. The logic of events is a formal method to describe the protocol state transition and algorithm in concurrent and distributed systems, which can be used to prove the security of network protocols. Based on logic of events, we propose migration rule and derive inheritability to reduce redundancy and complexity of protocol analysis procedure and improve efficiency of protocol analysis. We study the KerNeeS protocol which providing mutual authentication between POS and NFC phone, and conclude that the protocol can guarantee mutual authentication property between entities involved in the payment for secure payment transactions. The logic of events can be applied to the formal analysis of similar mobile payment protocols.

Resolution as a famous rule of inference has played a key role in automated reasoning for over five decades. A number of variants and refinements of resolution have been also studied, essentially, they are all based on binary resolution, that is, the cutting rule of the complementary pair while every deduction involves only two clauses. In the present work, we consider an extension of binary resolution rule, which is proposed as a novel contradiction separation based inference rule for automated deduction, targeted for dynamic and multiple (two or more) clauses handling in a synergized way, while binary resolution is its special case. This contradiction separation based dynamic multi-clause synergized automated deduction theory is then proved to be sound and complete. The development of this new extension is motivated not only by our view to show that such a new rule of inference can be generic, but also by our wish that this inference rule could provide a basis for more efficient automated deduction algorithms and systems.

SAT problem is the first proved NP-complete problems. Heuristic methods on solving the SAT problem although belongs to incomplete method, but it has its advantages. Genetic Algorithm (GA) as one of the heuristic algorithms, was applied to solve the SAT problem of many years, and also got some better results combine with other algorithms. However, there is still room for improvement. In this paper we combine GA with the Local Search Algorithm (LSA) and improve the sort algorithm. Using the Open MP to implement the Parallel Hybrid GA based on the Coarse-Grained Model (CGPHGA). This article describes the design and implementation of CGPHGA in detail, According to the experimental results, CGPHGA improves the success rate and efficiency.