F.M.: Large scale skill matching through knowledge compilation
- Eufemia Tinelli; Simona Colucci; Silvia Giannini; Eugenio Di Sciascio; M. Donini
Abstract. We present a logic-based framework for automated skill matching, able to return a ranked referral list and the related ranking explanation. Thanks to a Knowledge Compilation approach, a knowledge base in Description Logics is translated into a relational database, without loss of information. Skill matching inference services are then efficiently executed via SQL queries. Experimental results for scalability and turnaround times on large scale data sets are reported, confirming the validity of the approach. 1
A Linear/Producer/Consumer model of Classical Linear Logic
- Jennifer Paykin; Stephan A. Zdancewic; Jennifer Paykin; Steve Zdancewic
This paper defines a new proof- and category-theoretic framework for classical linear logic that separates reasoning into one linear regime and two persistent regimes corresponding to! and?. The resulting linear/ producer/consumer (LPC) logic puts the three classes of propositions on the same semantic footing, following Benton's linear/non-linear formulation of intuitionistic linear logic. Semantically, LPC corresponds to a system of three categories connected by adjunctions that reflect the linear/producer/consumer structure. The paper's metatheoretic results include admissibility theorems for the cut and duality rules, and a translation of the LPC logic into the category theory. The work also presents several concrete instances...
A really temporal logic
- Rajeev Alur; Thomas; A. Henzinger
Abstract. We introduce a temporal logic for the specification of real-time systems. Our logic, TPTL, employs a novel quantifier construct for referencing time: the freeze quantifier binds a variable to the time of the local temporal context. TPTL is both a natural language for specification and a suitable formalism for verification. We present a tableau-based decision procedure and a model-checking algorithm for TPTL. Several genemlizations of TPTL are shown to be highly undecidable.
Final version in Post-Workshop Proceedings UML98, Springer Verlag1 Reflections on the Object Constraint Language
- Ali Hamie; Franco Civello; John Howse; Stuart Kent; Richard Mitchell
Abstract. The Object Constraint Language (OCL), which forms part of the UML set of modelling notations, is a precise, textual language for expressing constraints that cannot be shown diagrammatically in UML. This paper reflects on a number of aspects of the syntax and semantics of the OCL, and makes proposals for clarification or extension. Specifically, the paper suggests that: the concept of flattening collections of collections is unnecessary, state models should be connectable to class models, defining object creation should be made more convenient, OCL should be based on a 2-valued logic, set subtraction should be covered more fully, and...
The LogAnswer Project at QA4MRE 2012
Abstract. For QA4MRE 2012, we have improved our prototype of a pure logic-based answer validation system that was originally developed for QA4MRE 2011. The system uses core functionality of the LogAnswer question answering (QA) system available on the web, which was com-bined and extended such as to best meet the demands of the QA4MRE task. In particular, coreference resolution is used in order to allow knowl-edge processing on the document level, and a fragment of OpenCyc has been integrated in order to allow more flexible reasoning. In addition to a general consolidation of the original prototype that took part in...
An Instantiation-Based Theorem Prover for First-Order Programming
First-order programming (FOP) is a new representation language that combines the strengths of mixed-integer linear program-ming (MILP) and first-order logic (FOL). In this paper we describe a novel feasibil-ity proving system for FOP formulas that combines MILP solving with instance-based methods from theorem proving. This prover allows us to perform lifted inference by re-peatedly refining a propositional MILP. We prove that this procedure is sound and refu-tationally complete: if a formula is infeasible our solver will demonstrate this fact in finite time. We conclude by demonstrating an im-plementation of our decision procedure on a simple first-order planning problem. 1
1 ON THE SYSTEM ANALYSIS OF THE FOUNDATIONS OF TRIGONOMETRY
- Temur Z. Kalanov
Abstract. Analysis of the foundations of standard trigonometry is proposed. The unity of formal logic and of rational dialectics is methodological basis of the analysis. It is shown that the foundations of trigonometry contradict to the principles of system approach and contain formal-logical errors. The principal logical error is that the definitions of trigonometric functions represent quantitative relationships between the different qualities: between qualitative determinacy of angle and qualitative determinacy of rectilinear segments (legs) in rectangular triangle. These relationships do not satisfy the standard definition of mathematical function because there are no mathematical operations that should be carry out on...
A Self-Applicable Partial Evaluator for the Logic Programming Language Godel
- Corin Alistair Gurr
Partial evaluation is a program specialisation technique that has been shown to have great potential in logic programming, particularly for the specialisation of meta-interpreters by the so-called “Futamura Projections”. Meta-interpreters and other meta-programs are programs which use another program as data. In this thesis we describe a partial evaluator for meta-programs in the logic programming language Gödel. Gödel is a declarative, general-purpose language which provides a number of higher-level programming features, including extensive support for meta-programming with a ground representation. The ground representation is a standard tool in mathematical logic in which object level variables are represented by ground terms...
Published In Submitted to POPL ’09 Dependently Typed Programming with Domain-Specific Logics
- Daniel R. Licata; Robert Harper; Daniel R. Licata; Robert Harper
We define a dependent programming language in which program-mers can define and compute with domain-specific logics, such as an access-control logic that statically prevents unauthorized access to controlled resources. Our language permits programmers to de-fine logics using the LF logical framework, whose notion of bind-ing and scope facilitates the representation of the consequence re-lation of a logic, and to compute with logics by writing functional programs over LF terms. These functional programs can be used to compute values at run-time, and also to compute types at compile-time. In previous work, we studied a simply-typed framework for representing and computing with...
Hygienic Macros for ACL2
- Carl Eastlund; Matthias Felleisen; Carl Eastlund; Matthias Felleisen
Abstract. ACL2 is a theorem prover for a purely functional subset of Common Lisp. It inherits Common Lisp’s unhygienic macros, which are used pervasively to eliminate repeated syntactic patterns. The lack of hygiene means that macros do not automatically protect their producers or consumers from accidental variable capture. This paper demonstrates how this lack of hygiene interferes with theorem proving. It then explains how to design and implement a hygienic macro system for ACL2. An evaluation of the ACL2 code base shows the potential impact of this hygienic macro system on existing libraries and practices. 1 Unhygienic Macros Are Not...
Proof Search in Lax Logic
- Jacob M. Howe
Abstract. A Gentzen sequent calculus for Lax Logic is presented, the proofs in which naturally correspond in a 1–1 way with the normal natural deductions for the logic. The propositional fragment of this calculus is then used a basis for another calculus, one which uses a history mechanism in order to give a decision procedure for propositional Lax Logic. 1
North-Holland Publishing Company THE TYPED A-CALCULUS IS NOT ELEMENTARY RECURSIVE
- Richard Statman; Communicated A. Meyer; R. Statman
Abstract. We prove that the problem of deciding for closed turns tl, t2 of the typed A-calculus whether tl &converts to t2 is not elementary recursive. 1. Intmdwtion Historically, the principal interest in the typed A-calculus is in connection with Giidel’s functional (“Dialectica”: see Giidel ) interpretation of intuitionistic arithmetic. However, since the early sixties interest has shifted to a wide variety of applications in diverse branches of logic, algebra and computer science. For example, in proof-theory (see for example, Tait ), in constructive logic (see for example, Lauchli [lo]), in the theory of functionals (see for example, Friedman ),...
Notion of Neutrosophic Risk and Financial Markets Prediction
- Dr. Sukanto Bhattacharya
In this paper we present an application of the neutrosophic logic in the prediction of the financial markets. 1.
To appear in the International Symposium on Microarchitecture Haifa Israel Exploiting ILP in PageBased Intelligent Memory
- Mark Oskin; Justin Hensley; Diana Keen; Frederic T Chong; Matthew Farrens; Aneet Chopra
This study compares the speed area and power of dier ent implementations of Active Pages OCS an intelligent memory system which helps bridge the growing gap between processor and memory performance by associating simple functions with each page of data Previous investigations have shown up to X speedups using a block of recong urable logic to implement these functions next to each sub array on a DRAM chip In this study we show that instructionlevel parallelism not hardware specialization is the key to the previous suc cess with recongurable logic In order to demonstrate this fact an Active Page...
Single-Spin Devices and the Foundations of Quantum Mechanics
- Alan M. Kadin
It is well known that electron spin is quantized, and is measured to be either spin up or spin down in a magnetic field, as was first demonstrated in the classic Stern-Gerlach experiment almost 100 years ago. However, it is also believed that a quantum spin may be indeterminate until it is measured, being in a quantum superposition of the two quantum states. On the contrary, I propose (based on a locally realistic spin-quantized picture of quantum waves) that an electron quantum state is always either spin up or spin down, but is never in a superposition of the two....
Lazy Set-Sharing Analysis
- Xuan Li; Andy King; Lunjin Lu
Abstract. Sharing analysis is widely deployed in the optimisation, spe-cialisation and parallelisation of logic programs. Each abstract unifica-tion operation over the classic Jacobs and Langen domain involves the calculation of a closure operation that has exponential worst-case com-plexity. This paper explores a new tactic for improving performance: laziness. The idea is to compute partial sharing information eagerly and recover full sharing information lazily. The net result is an analysis that runs in a fraction of the time of the classic analysis and yet has compa-rable precision. 1
- Carolyn Talcott
Abstract. Pathway Logic (PL) is an approach to modeling and analysis of bio-logical processes based on rewriting logic. This tutorial describes the use of PL to model signal transduction processes. It begins with a general discussion of Symbolic Systems Biology, followed by some background on rewriting logic and signal transduction. The representation and analysis of a small model Ras and Raf activation is presented in some detail. This is followed by discussion of a curated model of early signaling events in response to Epidermal Growth Factor stimulation.
- Giorgio Laguzzi
My research project regards the interconnection between two burgeoning areas of mathematical logic: generalized descriptive set theory and set theory of the κ-reals. 1 State of the art and preliminary work State of the art. Set theory is a branch of mathematical logic, which has been extensively developed during the 20th century as a foundation of mathematics. Two important subbranches are the set theory of the real numbers and the descriptive set theory, which concern a carefully investi-gation of definable subsets of the real line. In particular, one of the main purposes was to analyze how much regularity one could...
Towards Logic-Based Question Answering under Time Constraints
Abstract—Using logic for question answering (QA) promises more accurate answers and increased flexi-bility of querying. However, the computational effort for a deep linguistic analysis of the involved natural language (NL) expressions and the subsequent logical inferencing makes it difficult to leverage this power for real-time QA. The paper attributes this difficulty in part to the popular answer validation paradigm, and it proposes a different solution which avoids parsing of answers at query time. The novel approach, which uses logic for assessing the relevance of extracted pas-sages, allows better concurrency of QA subtasks since logic-based passage filtering can run in parallel...
1 Proof that an Infinite Number of Mersenne Prime Numbers Exit
- Stephen Marshall
This paper presents a complete and exhaustive proof of the infinitude of Mersenne prime numbers. The approach to this proof uses same logic that Euclid used to prove there are an infinite number of prime numbers. Then we prove that if p> 1 and d> 0 are integers, that p and p + d are both primes if and only if for integer n (see reference 1 and 2):