We propose a new graph-based spatial temporal logic for knowledge representation and automated reasoning in this paper. The proposed logic achieves a balance between expressiveness and tractability in applications such as cognitive robots. The satisfiability of the proposed logic is decidable. We apply a Hilbert style axiomatization for the proposed graph-based spatial temporal logic, in which Modus ponens and IRR are the inference rules. We show that the corresponding deduction system is sound and complete and can be implemented through SAT.
This paper presents a formal theory which describes propositional binary logic as a semantically closed formal language, and allows for syntactically and semantically well-formed formulae, formal proofs (demonstrability in Hilbertian acception), deduction (Gentzen's view of demonstrability), CNF-ization, and deconstruction to be expressed and tested in the same (computational) formal language, using the same data structure. It is also shown here that Cognitive Binary Logic is a self-described theory in which the Liar Paradox is deconstructed.
Computer Science, `Spiru Haret' University, Bucharest, Romania Faculty of Engineering, `Aurel Vlaicu' University, Arad, Romania
The relation between self awareness and intelligence is an open problem these days. Despite the fact that self awarness is usually related to Emotional Intelligence, this is not the case here. The problem described in this paper is how to model an agent which knows (Cognitive) Binary Logic and which is also able to pass (without any mistake) a certain family of Turing Tests designed to verify its knowledge and its discourse about the modal states of truth corresponding to well-formed formulae within the language of Propositional Binary Logic.
This paper presents Non-Axiomatic Term Logic (NATL) as a theoretical computational framework of humanlike symbolic reasoning in artificial intelligence. NATL unites a discrete syntactic system inspired from Aristotle's term logic and a continuous semantic system based on the modern idea of distributed representations, or embeddings. This paper positions the proposed approach in the phylogeny and the literature of logic, and explains the framework. As it is yet no more than a theory and it requires much further elaboration to implement it, no quantitative evaluation is presented. Instead, quali…
The automated proof search system and decidability for logic of correlated knowledge is presented in this paper. The core of the proof system is the sequent calculus with the properties of soundness, completeness, admissibility of cut and structural rules, and invertibility of all rules. The proof search procedure based on the sequent calculus performs automated terminating proof search and allows us to achieve decision result for logic of correlated knowledge.
This paper presents a distributed agent-based automated theorem proving framework based on order-sorted first-order logic. Each agent in our framework has its own knowledge base, communicating to its neighboring agent(s) using message-passing algorithms. The communication language between agents is restricted in such a manner that each agent can only communicate to its neighboring agent(s) by means of their common language. In this paper we provide a refutation-complete report procedure for automated theorem proving in order-sorted first-order logic in a subclass of distributed agent-based net…
In the present work I introduce a semantics based on the cognitive attitudes of acception and rejection entertained by a given society of agents for logics inspired on Dunn and Belnap's First Degree Entailment ($\mathbf{E}$). In contrast to the epistemic situations originally employed by $\mathbf{E}$, the cognitive attitudes do not coincide with truth-values and they seem more suitable to logics that intend to consider the informational content of propositions "said to be true" as well as of propositions "said to be false" as determinant of the notion of logical validity. After analyzing some …
We consider the setting of stochastic multiagent systems modelled as stochastic multiplayer games and formulate an automated verification framework for quantifying and reasoning about agents' trust. To capture human trust, we work with a cognitive notion of trust defined as a subjective evaluation that agent A makes about agent B's ability to complete a task, which in turn may lead to a decision by A to rely on B. We propose a probabilistic rational temporal logic PRTL*, which extends the probabilistic computation tree logic PCTL* with reasoning about mental attitudes (beliefs, goals and inten…
I propose a system for Automated Theorem Proving in higher order logic using deep learning and eschewing hand-constructed features. Holophrasm exploits the formalism of the Metamath language and explores partial proof trees using a neural-network-augmented bandit algorithm and a sequence-to-sequence model for action enumeration. The system proves 14% of its test theorems from Metamath's set.mm module.
Termination is an important and well-studied property for logic programs. However, almost all approaches for automated termination analysis focus on definite logic programs, whereas real-world Prolog programs typically use the cut operator. We introduce a novel pre-processing method which automatically transforms Prolog programs into logic programs without cuts, where termination of the cut-free program implies termination of the original program. Hence after this pre-processing, any technique for proving termination of definite logic programs can be applied. We implemented this pre-processing…
This workshop brings together practioners and researchers who are involved in the everyday aspects of logical systems based on higher-order logic. We hope to create a friendly and highly interactive setting for discussions around the following four topics. Implementation and development of proof assistants based on any notion of impredicativity, automated theorem proving tools for higher-order logic reasoning systems, logical framework technology for the representation of proofs in higher-order logic, formal digital libraries for storing, maintaining and querying databases of proofs. We envisi…
Freie Universität Berlin（柏林自由大学）；Cambridge University（剑桥大学）
We present an automated verification of the well-known modal logic cube in Isabelle/HOL, in which we prove the inclusion relations between the cube's logics using automated reasoning tools. Prior work addresses this problem but without restriction to the modal logic cube, and using encodings in first-order logic in combination with first-order automated theorem provers. In contrast, our solution is more elegant, transparent and effective. It employs an embedding of quantified modal logic in classical higher-order logic. Automated reasoning tools, such as Sledgehammer with LEO-II, Satallax and …
Probabilistic logic reasoning is a central component of such cognitive architectures as OpenCog. However, as an integrative architecture, OpenCog facilitates cognitive synergy via hybridization of different inference methods. In this paper, we introduce a differentiable version of Probabilistic Logic networks, which rules operate over tensor truth values in such a way that a chain of reasoning steps constructs a computation graph over tensors that accepts truth values of premises from the knowledge base as input and produces truth values of conclusions as output. This allows for both learning …
The purpose of this paper is to develop further the main concepts of Phenomena Dynamic Logic (P-DL) and Cognitive Dynamic Logic (C-DL), presented in the previous paper. The specific character of these logics is in matching vagueness or fuzziness of similarity measures to the uncertainty of models. These logics are based on the following fundamental notions: generality relation, uncertainty relation, simplicity relation, similarity maximization problem with empirical content and enhancement (learning) operator. We develop these notions in terms of logic and probability and developed a Probabili…
We report on several scenarios of using automated theorem proving software in university education. In particular, we focus on using the Theorema system in a software-enhanced logic-course for students in computer science or artificial intelligence. The purpose of using logic-software in our teaching is not to teach students the proper use of a particular piece of software. In contrast, we try to employ certain software in order to spark students' motivation and to support their understanding of logic principles they are supposed to understand after having passed the course. In a sense, we try…
This paper presents a method for synthesising sound and complete tableau calculi. Given a specification of the formal semantics of a logic, the method generates a set of tableau inference rules that can then be used to reason within the logic. The method guarantees that the generated rules form a calculus which is sound and constructively complete. If the logic can be shown to admit finite filtration with respect to a well-defined first-order semantics then adding a general blocking mechanism provides a terminating tableau calculus. The process of generating tableau rules can be completely aut…
In this paper we investigate further the tableaux system for a deontic action logic we presented in previous work. This tableaux system uses atoms (of a given boolean algebra of action terms) as labels of formulae, this allows us to embrace parallel execution of actions and action complement, two action operators that may present difficulties in their treatment. One of the restrictions of this logic is that it uses vocabularies with a finite number of actions. In this article we prove that this restriction does not affect the coherence of the deduction system; in other words, we prove that the…
We present a sequent-based deductive system for automatically proving entailments in separation logic by using mathematical induction. Our technique, called mutual explicit induction proof, is an instance of Noetherian induction. Specifically, we propose a novel induction principle on a well-founded relation of separation logic model and follow the explicit induction methods to implement this principle as inference rules, so that it can be easily integrated into a deductive system. We also support mutual induction, a natural feature of implicit induction, where the goal entailment and other en…
RWTH Aachen（亚琛工业大学）；TU Eindhoven（埃因霍温理工大学）；University of Innsbruck（因斯布鲁克大学）
There are two kinds of approaches for termination analysis of logic programs: "transformational" and "direct" ones. Direct approaches prove termination directly on the basis of the logic program. Transformational approaches transform a logic program into a term rewrite system (TRS) and then analyze termination of the resulting TRS instead. Thus, transformational approaches make all methods previously developed for TRSs available for logic programs as well. However, the applicability of most existing transformations is quite restricted, as they can only be used for certain subclasses of logic p…
Universität Koblenz-Landau（科布伦茨-兰道大学）；Harz University of Applied Sciences（哈尔茨应用科学大学）
Deontic logic is a very well researched branch of mathematical logic and philosophy. Various kinds of deontic logics are considered for different application domains like argumentation theory, legal reasoning, and acts in multi-agent systems. In this paper, we show how standard deontic logic can be used to model ethical codes for multi-agent systems. Furthermore we show how Hyper, a high performance theorem prover, can be used to prove properties of these ethical codes.
In the last two decades, modal and description logics have been applied to numerous areas of computer science, including knowledge representation, formal verification, database theory, distributed computing and, more recently, semantic web and ontologies. For this reason, the problem of automated reasoning in modal and description logics has been thoroughly investigated. In particular, many approaches have been proposed for efficiently handling the satisfiability of the core normal modal logic K(m), and of its notational variant, the description logic ALC. Although simple in structure, K(m)/AL…
Separation Logic with inductive definitions is a well-known approach for deductive verification of programs that manipulate dynamic data structures. Deciding verification conditions in this context is usually based on user-provided lemmas relating the inductive definitions. We propose a novel approach for generating these lemmas automatically which is based on simple syntactic criteria and deterministic strategies for applying them. Our approach focuses on iterative programs, although it can be applied to recursive programs as well, and specifications that describe not only the shape of the da…
Undergraduate students of artificial intelligence often struggle with representing knowledge as logical sentences. This is a skill that seems to require extensive practice to obtain, suggesting a teaching strategy that involves the assignment of numerous exercises involving the formulation of some bit of knowledge, communicated using a natural language such as English, as a sentence in some logic. The number of such exercises needed to master this skill is far too large to allow typical artificial intelligence course teaching teams to provide prompt feedback on student efforts. Thus, an automa…
Correctness and robustness are essential for logic synthesis applications, but they are often only tested with a limited set of benchmarks. Moreover, when the application fails on a large benchmark, the debugging process may be tedious and time-consuming. In some fields such as compiler construction, automatic testing and debugging tools are well-developed to support developers and provide minimal guarantees on program quality. In this paper, we adapt fuzz testing and delta debugging techniques and specialize them for gate-level netlists commonly used in logic synthesis. Our toolkit improves o…
IBM Research（IBM研究院）；MIT-IBM Watson AI Lab（麻省理工学院-IBM沃森人工智能实验室）；Northwestern University（西北大学）
Automated theorem proving in first-order logic is an active research area which is successfully supported by machine learning. While there have been various proposals for encoding logical formulas into numerical vectors -- from simple strings to more involved graph-based embeddings -- little is known about how these different encodings compare. In this paper, we study and experimentally compare pattern-based embeddings that are applied in current systems with popular graph-based encodings, most of which have not been considered in the theorem proving context before. Our experiments show that t…
National Institute of Informatics（国立情报学研究所）；Kyoto University（京都大学）
This work explores the application of deep learning, a machine learning technique that uses deep neural networks (DNN) in its core, to an automated theorem proving (ATP) problem. To this end, we construct a statistical model which quantifies the likelihood that a proof is indeed a correct one of a given proposition. Based on this model, we give a proof-synthesis procedure that searches for a proof in the order of the likelihood. This procedure uses an estimator of the likelihood of an inference rule being applied at each step of a proof. As an implementation of the estimator, we propose a prop…
The problem-solving in automated theorem proving (ATP) can be interpreted as a search problem where the prover constructs a proof tree step by step. In this paper, we propose a deep reinforcement learning algorithm for proof search in intuitionistic propositional logic. The most significant challenge in the application of deep learning to the ATP is the absence of large, public theorem database. We, however, overcame this issue by applying a novel data augmentation procedure at each iteration of the reinforcement learning. We also improve the efficiency of the algorithm by representing the syn…
Conflict-Aware Fusion: Mitigating Logic Inertia in Large Language Models via Structured Cognitive Priors
Xtracta & Strong AI Lab, University of Auckland（Xtracta与强人工智能实验室，奥克兰大学）；School of Humanities, China University of Political Science and Law（人文学院，中国政法大学）；Strong AI Lab, University of Auckland（强人工智能实验室，奥克兰大学）
These proceedings contain the papers presented at the 10th International Workshop on Automated Specification and Verification of Web Systems (WWV 2014), which was held on 18 July 2014 in Vienna, Austria, as a satellite workshop of the Federated Logic Conference (FLoC 2014), associated to the 7th International Joint Conference on Automated Reasoning (IJCAR 2014), as part of the Vienna Summer of Logic (VSL 2014). WWV is a yearly workshop that aims at providing an interdisciplinary forum to facilitate the cross-fertilization and the advancement of hybrid methods that exploit concepts and tools dr…
Ladder Logics is a programming language standardized in IEC 61131-3 and widely used for programming industrial Programmable Logic Controllers (PLC). A PLC program consists of inputs (whose values are given at runtime by factory sensors), outputs (whose values are given at runtime to factory actuators), and the logical expressions computing output values from input values. Due to the graphical form of Ladder programs, and the amount of inputs and outputs in typical industrial programs, debugging such programs is time-consuming and error-prone. We present, in this paper, a Why3-based tool protot…
Outsourcing of complex IT infrastructure to IT service providers has increased substantially during the past years. IT service providers must be able to fulfil their service-quality commitments based upon predefined Service Level Agreements (SLAs) with the service customer. They need to manage, execute and maintain thousands of SLAs for different customers and different types of services, which needs new levels of flexibility and automation not available with the current technology. The complexity of contractual logic in SLAs requires new forms of knowledge representation to automatically draw…
