The standard contradiction separation (S-CS) rule is a new inference rule recently proposed in the field of automated reasoning, which is characterized by dynamism, robustness, and collaborative deduction of multiple clauses. According to the above characteristics, to further utilize the inference ability of the S-CS rule, we propose an inverse and parallel algorithms to extend and enhance S-CS rule. Specifically, a multi-layer inverse and parallel deduction algorithm (in short MIP) is built. This algorithm transforms the first-order logic clause set into multiple clause sets, which are then recursively and iteratively deduced in parallel such that whenever a clause set is unsatisfiable, the original clause set is unsatisfiable. The main advantages of this algorithm are inverse deduction, parallel deduction, and depth (multi-layer) deduction. In order to improve the performance of automated theorem prover, we embed this algorithm into the current top automated theorem provers Vampire and E to form the new provers MIP_V and MIP_E. Then we test MIP_V with the problems from the international competition (CASC) for automated theorem provers, and test MIP_E and MIP_V with the hardest problem of rating = 1 from the benchmark library TPTP. The experimental results show that MIP_V (MIP_E) has a better performance than Vampire (E), and MIP_V and MIP_E can solve 66 problems with rating = 1.
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.
The high risk associated with industrial water use and the asymmetry of accident consequences shape decision-makers’ strong aversion to losses. However, existing water resource vulnerability (WRV) assessments often overlook decision-makers’ risk aversion and system resilience. To address this, this study develops an industrial-driven regional water vulnerability (IDRWV) framework integrating Driving Force-Pressure-State-Impact-Response-Resilience (DPSIRR) diagnosis, stochastic Deck of Cards (DoC)-CRITIC weighting, and prospect-theory-based K-means-TODIMSort classification. This framework distinguishes external response from endogenous resilience, quantifies expert cognitive divergence, and captures loss-averse vulnerability sorting. Anhui Province in China, a typical industrial-agricultural composite region, serves as the case study. Results indicate that the provincial IDRWV score increases from 0.5013 in 2012 to 0.8086 in 2023, while the number of cities reaching Level V or above rises from 1 to 13. The 2020 peak score of 0.8312 reveals the short-term effect of end-of-pipe treatment, but source reduction remains a bottleneck. Industrial wastewater environmental load ratio (q=0.6868) and total industrial wastewater discharge (q=0.6015) are the dominant drivers, indicating a shift from discharge-volume control to load-capacity mismatch management. The rigid industrial structure of heavy industrial cities along the Yangtze River causes their IDRWV improvement to lag behind, making resilience building the key to overcoming their developmental challenges. This study reveals that the key to the transformation of industrialized cities lies in establishing a water resource resilience system that aligns with industrial structures through adaptive management.
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.
In complex system modeling, the Belief Rule Base (BRB) integrates expert knowledge with data-driven approaches, offering strong interpretability. However, conventional BRB models face challenges such as rule explosion, parameter optimization difficulties, and the trade-off between interpretability and accuracy. Introducing the concept of backpropagation into BRB is of great significance, as combining BRB with gradient descent enables rapid convergence and efficient parameter optimization. This study proposes a backpropagation BRB(BP-BRB) method with parameterized rule center construction. Experiments on 23 public datasets demonstrate that BP-BRB improves training efficiency, enhances generalization ability, and achieves superior performance compared to standard BRB models and existing rule-based reasoning methods, thereby validating the novelty and effectiveness of the proposed approach.
Large language models (LLMs) achieve impressive benchmark performance yet exhibit systematic gaps in realworld deployment contexts. This is particularly concerning for AI governance applications where LLMs might identify risk categories but fail to trace the causal mechanisms through which harms actually unfold. We propose that structuring documented AI risks as explicit causal patterns-sequential mechanisms, feedback loops, and quantified effects from empirical researchcan scaffold more reliable LLM reasoning through human-AI collaboration. We test this through a controlled study comparing pattern-augmented LLMs against vanilla LLMs using GPT-4o and Grok 4 to analyse five real estate AI deployment cases. Results show substantial improvements: GPT-4o improved in causal depth with Cohen’s $d=1.20$, while Grok showed even larger effects ($d=1.93$) alongside improved evidence grounding ($d=2.10$). Validation using Gemini 2.5 Pro and DeepSeek as judges confirmed findings with moderate-to-high inter-rater agreement ($r=0.45$ to 0.68). Qualitative analysis reveals explicit mechanistic transfer, with augmented outputs mapping patterns from domains such as aviation automation and reinforcementlearning pricing to novel real estate contexts. These findings suggest that structured causal knowledge can enable a new modality of human-AI collaboration for AI risk assessment.
Complex topological relationships exist between large amounts of dynamic fuzzy data and linguistic-valued data in real-world scenarios. Although existing graph neural network models can incorporate structural information, they struggle to effectively handle dynamic fuzzy data when the underlying graph structure is not explicitly available. To address these challenges, this study proposes a dynamic fuzzy linguistic-valued topological graph attention network (DFLVT-GAT) that captures structural relationships among objects within the underlying topological framework. First, the dynamic fuzzy linguistic-valued concept lattice is constructed for the corresponding formal context to reveal the conceptual hierarchy of dynamic fuzzy linguistic-valued data and linguistic-valued data. Second, a preprocessing module for DFLVT-GAT is developed based on dynamic fuzzy linguistic-valued topology (DFLVT), into which an attention mechanism is integrated to guide node updates. Additionally, graph data are transformed into a DFLVT under multi-granularity linguistic expressions by selecting different linguistic granularities. Finally, extensive experimental results on graph and multivariate datasets demonstrate the effectiveness of the proposed DFLVT-GAT for classification.
Prefabricated buildings, as a modern construction method, offer notable advantages such as high construction efficiency, superior thermal insulation, optimized spatial utilization, and enhanced energy and environmental performance. Compared with traditional cast-in-place techniques, the industrialized processes inherent in the embodied phase of prefabricated construction can significantly reduce carbon emissions. However, the modular nature of such systems introduces added complexity in managing emission reduction. To address uncertainties arising from subjective differences in expert judgments-due to varying professional backgrounds and knowledge structures-this study proposes a carbon emission evaluation model based on spherical fuzzy sets integrated with the Analytic Hierarchy Process (AHP). A comprehensive evaluation index system is established, encompassing seven key dimensions: project characteristics, material consumption, energy usage, transportation and storage, construction organization, ecological environment, and policy regulations. The Spherical Fuzzy Analytic Hierarchy Process (SF-AHP) is employed to develop a robust emission reduction efficiency model. The model is validated through application to a real-world prefabricated building project. Results demonstrate that the proposed approach enhances the objectivity and accuracy of carbon emission assessments in prefabricated construction, thereby supporting informed decision-making toward sustainable development goals.
In order to alleviate environmental problems, China has formulated the environmental protection tax law. However, how does its implementation affect the financial performance of enterprises? This paper selects A-share listed companies from 2012 to 2024 as the research sample from the massive data of China Stock Market & Accounting Research (CSMAR) database, and empirically studies the relationship between the implementation of environmental protection tax policies and corporate financial performance by using difference-in-differences big data analysis technology. The study found that the implementation of the environmental protection tax law policy is positively correlated with the financial performance of enterprises, and after a variety of data visualization robustness tests, the conclusion is still valid. Through the analysis of big data mechanism, we found that technological innovation and agency costs play a certain mediating effect between the two. In order to ensure the implementation of environmental protection tax, it is suggested to build a cross sectoral risk warning mechanism based on data sharing, and rely on the dynamic tax preference model to realize “the less pollution, the more preferential”, so as to stimulate the green innovation power of enterprises.
This paper addresses the problem of document-level event extraction as a critical step toward automated knowledge acquisition for intelligent systems. Extracting structured event knowledge from unstructured text is essential for downstream knowledge-based applications such as knowledge graph construction, decision support, and intelligent question answering. However, existing approaches struggle to effectively capture long-range dependencies and complex inter-event relationships within documents while maintaining computational efficiency. To address these challenges, we propose a novel knowledge-aware framework, the Graph Convolutional Network with Pseudo-trigger Combination Recognition(GCN-PCR). The proposed model explicitly represents entities, mentions, and sentences as interconnected nodes in a relational graph, enabling structured modeling of semantic dependencies and co-reference information across document contexts. Furthermore, the pseudo-trigger combination strategy enhances the identification of event structures by improving the robustness of event boundary detection and argument association. Extensive experiments on two public datasets demonstrate that the proposed approach achieves superior performance compared to state-of-the-art methods. More importantly, our framework provides a scalable and effective solution for transforming unstructured textual data into structured event knowledge, facilitating its integration into knowledge-based systems.
Agentic AI based on large language models (LLMs) is rapidly evolving from static chatbots to autonomous systems that plan, act, and interact with tools in open-ended environments. However, current LLM agents lack calibrated uncertainty, robust safety mechanisms, and faithful explanations, making them ill-suited for safety-critical settings such as healthcare, finance, cybersecurity, and industrial operations. Extended Belief Rule Bases (EBRB) are representative examples of interpretable, rule-based probabilistic reasoning frameworks with explicit representation of belief and ignorance, and have been successfully applied in complex decision problems without suffering from the rule explosion that affects traditional rule-based approaches. This position paper argues that EBRB could serve as a core safety and reasoning governor within LLM-based agentic pipelines, yielding hybrid systems to better align agentic AI systems with emerging regulatory and ethical requirements for Trustworthy AI (TAI) in high-risk settings. We outline: (i) a conceptual architecture integrating LLMs with EBRB in agentic workflows; (ii) the mapping from this architecture to TAI dimensions including transparency, uncertainty, safety, fairness, and auditability; (iii) concrete opportunities across healthcare, finance, cybersecurity, and industrial safety; and (iv) a research agenda highlighting open challenges in scalable rule induction, co-adaptation between LLMs and EBRB, and evaluation of hybrid agents. Our goal is not to present empirical benchmarks, but to articulate a vision and roadmap for EBRB-enhanced agentic AI that is both powerful and trustworthy.
When organisations deploy AI systems in high-stakes domains, they need risk assessments they can trust. Large language models offer a promising path to scalable assessment, but two problems undermine their reliability: shallow reasoning that flags risks without tracing causal mechanisms, and untuned aggregate output that sits systematically above cautious expert postures. We address both problems with a two-layer framework. Causal risk patterns structure the reasoning input: each pattern documents a known harm mechanism with its trigger conditions, causal steps, and empirical evidence. Ordered Weighted Averaging (OWA) calibrates the output by weighting multiple LLM assessments according to rank rather than source, systematically aligning aggregate output with a chosen expert calibration target. In experiments with three frontier LLMs assessing 125 case-pattern pairs across five real estate AI deployments, all models produced ratings sitting +0.07 to +0.16 above our expert target on a 0–1 scale. OWA aggregation calibrated to this target reduced mean absolute error by 7.7
High-stakes domains such as healthcare demand AI systems that are not only accurate but also transparent and aligned with established medical standards. Purely data-driven machine learning often fails on highly imbalanced medical datasets, overlooking critical minority cases, while traditional expert systems are rigid and inflexible. To address this, we introduce a neuro-symbolic framework, the “Hybrid Intelligent Extended Belief Rule Base (HI-EBRB),” which is based on the Extended Belief Rule Base (EBRB). Our approach combines explicit clinical guidelines with empirically weighted data through two complementary channels: an NLP-driven pipeline extracts knowledge from clinical texts (e.g., AHA/ACC guidelines), and a Complexity-Aware Weighting mechanism moderates the influence of rules derived from ambiguous or highly complex data. Transparency is further enhanced using a Balanced Rule Reduction algorithm to reduce the initial rule base. Tested on three imbalanced medical datasets (Stroke, PIMA, Framingham), the framework outperformed standard baselines, achieving an average Minority Recall of 0.81 and G-Mean of 0.68, while compressing over 97
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.
Multi-agent pathfinding and its reliable execution in stochastic environments represent a critical challenge for real-world applications, demanding both the planning of efficient paths and the formal assurance of safe, conflict-free operation. This paper introduces a novel methodology framework to address this dual requirement. To maximize operational efficiency, we introduce a strategy for optimal goal allocation for team collaboration, integrating it with the conflict-based search algorithm to minimize the total move counts required for mission completion. The second component is an integrated verification process grounded in probabilistic model checking. We model the multi-agent path execution process under stochastic uncertainties using a Markov decision process. By leveraging the probabilistic model checker and probabilistic computation tree logic, the framework formally verifies critical safety properties, ensuring conflict-free and deadlock-free path execution. Furthermore, it evaluates the effectiveness of proposed behavioral constraints designed to mitigate stochastic delays, thereby verifying the overall system safety. By fusing multi-agent planning, probabilistic reasoning, and formal logic-based verification, the proposed framework establishes a foundation amenable to natural extension for addressing multi-agent decision-making and uncertainty estimation. Case study results demonstrate that our methodology effectively selects the pathfinding solution with the minimum move count while significantly enhancing overall system safety through these formally verified behavioral constraints.
In fuzzy rough sets, the traditional approach primarily employs fuzzy rough approximation operators and fuzzy neighborhood operators to solve attribute reduction problems. However, measures constructed by these operators fail to capture the correlation between attributes, whereas the generalized Shapley value(SHV), as a non-additive measure, takes into account the correlation between attributes from a global perspective. Based on the global attribute correlation problems, SHV for fuzzy neighborhoods utilizing pseudo-overlap functions are proposed to deal with the problem of attribute reduction. Firstly, in the fuzzy beta covering approximation spaces(beta-FCASs), based on pseudo-overlap functions and their corresponding residual implications((IPO, PO)), (IPO, PO)-fuzzy beta neighborhood operators ((IPO, PO)-beta- FN operators) and four pairs of (IPO, PO) fuzzy beta neighborhood measures((IPO, PO)-fuzzy beta- NMs) based on these operators are constructed, thereby extending the representational capacity of fuzzy covering-based rough sets. Secondly, four pairs of SHVs utilize on (IPO, PO)-fuzzy beta- NMs are introduced to evaluate attribute significance from a global perspective. And a new method of attribute reduction of fuzzy beta covering information decision tables(beta-FCIDTs) based on SHV is proposed. Thirdly, four pairs of Choquet integrals(CHIs) based on SHV are constructed. On this basis, a method for addressing the attribute reduction of beta-FCIDT is proposed by considering the correlation of global attributes, and the proposed method is used to deal with the classification problem specifically. Finally, the validity and practicality of the proposed methods are confirmed through the use of several public datasets.
The formalization of natural language into first-order logic (FOL) is a key challenge in integrating large language models (LLMs) with symbolic reasoning systems. While recent approaches show promising translation capabilities, LLM-generated formulas often suffer from syntactic errors and structural inconsistencies that hinder downstream verification. In this paper, we propose a neural-symbolic framework for bidirectional conversion between natural language and TPTP-formatted FOL formulas. Our approach integrates the E automated theorem prover into an iterative verification-repair loop, where parser diagnostics and verification feedback guide the correction of LLM-generated formulas. We implement a fully automated batch pipeline and evaluate it on 652 TPTP problems across multiple LLM backbones. Experimental results show that prover-guided correction substantially improves the rate of syntactically valid and verifiable conversions. Although semantic equivalence remains challenging, the results demonstrate the value of combining neural generation with symbolic verification to enhance robustness in formal logic translation.
Granular computing enhances the modeling capability of rough sets through efficient data granulation. While granular-ball rough sets offer a flexible representation, existing models treat all granular balls equally, ignoring their varying relevance to classification outcomes. To overcome this limitation, we propose a weighted granular-ball rough set (WGBRS) model, along with a novel granular learning framework for feature selection and fault diagnosis. First, by introducing a weighting mechanism into granular balls, the WGBRS model is established to achieve a finer approximation of knowledge boundaries and overcome the limitation of existing granular-ball computing, where all granular balls are treated with equal weight. Second, based on the WGBRS model, a heuristic feature selection algorithm is developed, leveraging weighted dependency measures to efficiently eliminate redundant attributes while preserving key classification information. Finally, compared with traditional feature selection methods (including those based on rough set and granular-ball rough set models), the feature selection approach based on WGBRS achieves higher classification accuracy across multiple datasets. The robustness and practical effectiveness of the method are further validated through a real-world rolling bearing fault diagnosis application with added noise, confirming the advantages of incorporating granular-ball weights within the proposed framework.
Da Ruan合作论文数Department of Applied Mathematics & Computer Science;Fuzziness and Uncertainty Modelling Research Unit40