The Use of Lemmas in the Model Elimination Procedure

When the model elimination (ME) procedure was first proposed, the notion of lemma was put forth as a promising augmentation to the basic complete proof procedure. Here the lemmas that are used are also discovered by the procedure in the same proof run. Several implementations of ME now exist, but only a 1970s implementation explicitly examined this lemma mechanism, with indifferent results. We report on the successful use of lemmas using the METEOR implementation of ME. Not only does the lemma device permit METEOR to obtain proofs not otherwise obtainable by METEOR, or any other ME prover not using lemmas, but some well-known challenge problems are solved. We discuss several of these more difficult problems, including two challenge problems for uniform general-purpose provers, where METEOR was first in obtaining the proof. The problems are not selected simply to show off the lemma device, but rather to understand it better. Thus, we choose problems with widely different characteristics, including one where very few lemmas are created automatically, the opposite of normal behavior. This selection points out the potential of, and the problems with, lemma use. The biggest problem normally is the selection of appropriate lemmas to retain from the large number generated.     

Autarky Pruning in Propositional Model Elimination Reduces Failure Redundancy

Goal-sensitive resolution methods, such as Model Elimination, have been observed to have a higher degree of search redundancy than model-search methods. Therefore, resolution methods have not been seen in high-performance propositional satisfiability testers. A method to reduce search redundancy in goal-sensitive resolution methods is introduced. The idea at the heart of the method is to attempt to construct a refutation and a model simultaneously and incrementally, based on subsearch outcomes. The method exploits the concept of autarky, which can be informally described as a self-sufficient model for some clauses, but which does not affect the remaining clauses of the formula. Incorporating this method into Model Elimination leads to an algorithm called Modoc. Modoc is shown, both analytically and experimentally, to be faster than Model Elimination by an exponential factor. Modoc, unlike Model Elimination, is able to find a model if it fails to find a refutation, essentially by combining autarkies. Unlike the pruning strategies of most refinements of resolution, autarky-related pruning does not prune any successful refutation; it only prunes attempts that ultimately will be unsuccessful; consequently, it will not force the underlying Modoc search to find an unnecessarily long refutation. To prove correctness and other properties, a game characterization of refutation search is introduced, which demonstrates some symmetries in the search for a refutation and the search for a model. Experimental data is presented on a variety of formula classes, comparing Modoc with Model Elimination and model-search algorithms. On random formulas, model-search methods are faster than Modoc, whereas Modoc is faster on structured formulas, including those derived from a circuit-testing application. Considerations for first-order refutation methods are discussed briefly.     

命题逻辑提升到一阶逻辑上的子句消去方法

在基于命题逻辑的可满足性问题（SAT）求解器和基于一阶逻辑的定理证明器上，子句集简化一直是必不可少的步骤，而其中子句消去方法在这些子句集简化方法中是非常重要的组成部分。将命题逻辑中的子句消去方法归结隐藏恒真消去方法（RHTE）和归结隐藏包含消去方法（RHSE）提升到一阶逻辑上，并且利用蕴含模归结原则（IMR）证明了这种提升方式在一阶逻辑上具有可靠性（Soundness），即依据这两种子句消去方法删除一阶逻辑公式集中的子句，并不会改变公式集的可满足性或者不可满足性。此外，将这两个方法与一阶逻辑子句消去方法锁子句消去方法（BCE）和归结包含消去方法（RSE）进行组合推广，发展得到一阶逻辑上新型子句消去方法（BC+RHS）E、（RS+RHT）E和（RHS+RHT）E，并且证明了这3种子句消去方法在一阶逻辑上的可靠性。最后，分析比较了这些子句消去方法的有效性，并且证明了这3种新型子句消去方法比组成它们的原始子句消去方法均具有更高的有效性。     

基于幂零泛与运算模型的命题模糊逻辑

本文讨论了泛与运算模型T(x,y．h)(h∈(o,0．75))的一些性质;证明了泛与运算模型T(x,y,h)(h∈(0,O.75))是一个幂零三角范数;而且泛与运算模型T(x,y．h)(h∈(0,0．75))与泛蕴涵运算模型,(x,y,h)(h∈(0,0.75))是一个伴随对;进一步证明了([0,1].∨,∧．*,→．0,1)作成一个MV-代数。给出了基于幂零泛与运算模型T(x,y,h)(h∈(0,0.75))的模糊命题演算系统PC(T),证明了此命题演算系统与Lukasiewicz逻辑命题演算系统是等价的。     

一个命题投影时序逻辑符号模型检测器

现有模型检测工具的形式化规范语言,如计算树逻辑(computation tree logic,简称CTL)和线性时序逻辑(linear temporal logic,简称LTL)等的描述能力不足,无法验证ω正则性质.提出了一个命题投影时序逻辑(propositional projection temporal logic,简称PPTL)符号模型检测工具——PLSMC(PPTL symbolic model checker)的设计与实现过程.该工具基于著名的符号模型检测系统NuSMV,实现了PPTL的符号模型检测算法.PLSMC的规范语言PPTL具有完全正则表达能力,这使得定性性质和定量性质均可被验证.此外,PLSMC可以有效地缓解模型检测工具中容易发生的状态空间爆炸问题.最后,利用PLSMC对铁路公路交叉道口护栏控制系统的安全性质和周期性性质进行验证.实验结果表明,PPTL符号模型检测工具扩充了NuSMV系统的验证能力,使得时间敏感、并发性和周期性等实时性质可以被描述和验证.     

T-Resolution: Refinements and Model Elimination

T-resolution is a binary rule, proposed by Policriti and Schwartz in 1995 for theorem proving in first-order theories (T-theorem proving) that can be seen – at least at the ground level – as a variant of Stickel's theory resolution. In this paper we consider refinements of this rule as well as the model elimination variant of it. After a general discussion concerning our viewpoint on theorem proving in first-order theories and a brief comparison with theory resolution, the power and generality of T-resolution are emphasized by introducing suitable linear and ordered refinements, uniformly and in strict analogy with the standard resolution approach. Then a model elimination variant of T-resolution is introduced and proved to be sound and complete; some experimental results are also reported. In the last part of the paper we present two applications of T-resolution: to constraint logic programming and to modal logic.     

Propositional Attitudes and Causation

Predicting and explaining the behavior of others in terms of mental states is indispensable for everyday life. It will be equally important for artificial agents. We present an inference system for representing and reasoning about mental states, and use it to provide a formal analysis of the false-belief task. The system allows for the representation of information about events, causation, and perceptual, doxastic, and epistemic states (vision,belief, and knowledge), incorporating ideas from the event calculus and multi-agent epistemic logic. Unlike previous AI formalisms, our focus here is on mechanized proofs and proof programmability, not on metamathematical results. Reasoning is performed via relatively cognitively plausible inference rules, and a degree of automation is achieved by generalpurpose inference methods and by a syntactic embedding of the system in first-order logic.     

Controlled Use of Clausal Lemmas in Connection Tableau Calculi

Proof procedures based on model elimination or the connection tableau calculus have become more and more successful. But these procedures still suffer from long proof lengths as well as from a rather high degree of redundant search effort in comparison with resolution-style search procedures. In order to overcome these problems we investigate the use of clausal lemmas. We develop a method to augment a given set of clauses by a lemma set in a preprocessing phase and discuss the ability of this technique to reduce proof lengths and depths and to provide an appropriate reordering of the search space. We deal with the basic connection tableau calculus as well as with several calculus refinements and extensions. In order to control the use of lemmas we develop techniques for selecting relevant lemmas based on partial evaluation techniques. Experiments with the prover Setheo performed in several domains demonstrate the high potential of our approach.     

Reasoning Processes in Propositional Logic

We conducted a computer-based psychological experiment in which a random mix of 40 tautologies and 40 non-tautologies were presented to the participants, who were asked to determine which ones of the formulas were tautologies. The participants were eight university students in computer science who had received tuition in propositional logic. The formulas appeared one by one, a time-limit of 45 s applied to each formula and no aids were allowed. For each formula we recorded the proportion of the participants who classified the formula correctly before timeout (accuracy) and the mean response time among those participants (latency). We propose a new proof formalism for modeling propositional reasoning with bounded cognitive resources. It models declarative memory, visual memory, working memory, and procedural memory according to the memory model of Atkinson and Shiffrin and reasoning processes according to the model of Newell and Simon. We also define two particular proof systems, T and NT, for showing propositional formulas to be tautologies and non-tautologies, respectively. The accuracy was found to be higher for non-tautologies than for tautologies (p < .0001). For tautologies the correlation between latency and minimum proof length in T was .89 and for non-tautologies the correlation between latency and minimum proof length in NT was .87.     

基于命题投影时序逻辑的单调速率调度算法模型检测

提出了基于命题投影时序逻辑(propositional projection temporal logic,简称PPTL)的单调速率调度(rate monotonic scheduling,简称RMS)模型检测方法.该方法使用SPIN模型检测器的系统建模语言PROMELA为任务调度系统建模,使用PPTL描述系统期望的性质,通过SPIN验证系统模型是否满足性质,从而得知一个任务组在RMS下是否可调度.同时,RMS算法控制下的任务调度系统的其他性质也可以得到验证.     

Propositional and terminological knowledge representations

Abstract

Formalisms based on a propositional representation demonstrate a high representational competence because of their flexibility, properties, and their great expression power, even if they often fail to represent the meaning of the nodes that make up the propositional networks. The presence of a network of definitions would make the representation richer, and would augment the expressiveness and the inferential capabilities of the whole system: the twofold architecture of the hybrid systems seems to be suitable to satisfy these prerequisites. Nevertheless, the hybrid systems fail to clearly define the intensional and extensional levels of knowledge. This paper proposes a different distribution of tasks between the two parts of a hybrid system on the ground of a precise distinction among intensional, mental extensional, and extensional aspects of knowledge. Moreover, it suggests employing a propositional approach also for arranging the abstract definitions of the terminological box. These principles have been tested in KRAM (Knowledge Representation for Agency Modelling), a hybrid system used as a component both of a cooperative interface and of a system able to model actions and minds of cognitive agents.     

一种基于并发命题投影时序逻辑模型检测的入侵检测方法

基于投影时序逻辑模型检测的入侵检测方法具有描述网络入侵者分段攻击的能力,然而对并发攻击仍无能为力,因为该逻辑无法直接描述并发。针对此问题,在该逻辑的基础上定义了一种新的并发算子,并给出基于并发投影时序逻辑模型检测的入侵检测方法。对复杂攻击实例的检测表明,新方法可有效提高对并发攻击的检测能力。     

Conflict-Driven Satisfiability for Theory Combination: Lemmas,Modules, and Proofs

Journal of Automated Reasoning - Search-based satisfiability procedures try to build a model of the input formula by simultaneously proposing candidate models and deriving new formulae implied by...     

基于高斯混合模型的空间域背景分离法及阴影消除法

运动检测和背景分离技术是智能视频监控系统中的一项关键技术。由于目前广泛使用的高斯混合模型背景分离法是在像素域的时间尺度上对像素进行分类,因此常常造成误判,且无法解决阴影问题。为解决此问题,提出了一种空间域上的背景分离法。该方法首先将像素检测从像素域拓展至空间域的局部窗口内;然后在得到前景点集后,再将此空间域检测思想结合像素亮度特征运用到阴影消除中;最后,对经典模型的部分参数估计方法进行了修改。相关的实验结果证明,该方法可用于提高背景分离的检测精度和实现运动物体阴影消除。     

基于极限树特征递归消除和LightGBM的异常检测模型

入侵检测数据维数大、数据样本不均衡、数据集分散性大的问题严重影响分类性能,为了解决该问题,文章提出基于极限随机树的特征递归消除(Extra Trees-Recursive Feature Elimination,ET-RFE)和LightGBM(LGBM)的入侵检测方法。首先对网络数据进行独热编码重构,在数据级层面均衡少量样本的攻击类别;其次,使用基于ET-RFE对流量特征进行降维处理,寻找含有信息量最大的最优特征子集;最后,将得到的最优特征子集作为LGBM输入数据集进行分类训练,并利用贝叶斯算法对LGBM参数进行优化。实验采用真实的网络流量数据集UNSW-NB15,通过与随机森林(RF)、XGboost算法和GALR-DT算法比较可得,文章所提方法能够有效提高检测率,并对小样本攻击类型实现有效的召回率。     

Speaking about Transitive Frames in Propositional Languages

This paper is a comparative study of the propositional intuitionistic (non-modal) and classical modal languages interpreted in the standard way on transitive frames. It shows that, when talking about these frames rather than conventional quasi-orders, the intuitionistic language displays some unusual features: its expressive power becomes weaker than that of the modal language, the induced consequence relation does not have a deduction theorem and is not protoalgebraic. Nevertheless, the paper develops a manageable model theory for this consequence and its extensions which also reveals some unexpected phenomena. The balance between the intuitionistic and modal languages is restored by adding to the former one more implication.