Mostrando recursos 1 - 20 de 2.375

  1. A logic of explicit knowledge

    Melvin Fitting
    A well-known problem with Hintikka-style logics of knowledge is that of logical omniscience. One knows too much. This breaks down into two subproblems: one knows all tautologies, and one’s knowledge is closed under consequence. A way of addressing the second of these is to move from knowledge simpliciter, to knowledge for a reason. Then, as consequences become ‘further away ’ from one’s basic knowledge, reasons for them become more complex, thus providing a kind of resource measurement. One kind of reason is a formal proof. Sergei Artemov has introduced a logic of explicit proofs, LP. I present a semantics for...

  2. Non-deterministic temporal logics for general flow systems

    J. M. Davoren; V. Coulthard; N. Markey; T. Moor
    Abstract. In this paper, we use the constructs of branching temporal logic to formalize reasoning about a class of general flow systems, including discretetime transition systems, continuous-time differential inclusions, and hybrid-time systems such as hybrid automata. We introduce Full General Flow Logic, GFL �, which has essentially the same syntax as the well-known Full Computation Tree Logic, CTL � , but generalizes the semantics to general flow systems over arbitrary time-lines. We propose an axiomatic proof system for GFL � and establish its soundness w.r.t. the general flow semantics. 1

  3. Improving Synthesis of Compressor Trees on FPGAs via Integer Linear Programming


    Multi-input addition is an important operation for many DSP and video processing applications. On FPGAs, multi-input addition has traditionally been implemented using trees of carry-propagate adders. This approach has been used because the traditional look-up table (LUT) structure of FPGAs is not amenable to compressor trees, which are used to implement multi-input addition and parallel multiplication in ASIC technology. In prior work, we developed a greedy heuristic method to map compressor trees onto the general logic of an FPGA using a component called generalized parallel counter (GPC). Although this technique reduced the combinational delay of our circuits, when synthesized onto...

  4. Muskens. Intensional models for the theory of types

    Muskens Reinhard; Link To Publication
    Citation for published version (APA): Muskens, R. A. (2007). Intensional models for the theory of types. The journal of symbolic logic, 72(1), 98-118. General rights Copyright and moral rights for the publications made accessible in the public portal are retained by the authors and/or other copyright owners and it is a condition of accessing publications that users recognise and abide by the legal requirements associated with these rights.? Users may download and print one copy of any publication from the public portal for the purpose of private study or research? You may not further distribute the material or use it...

  5. Geolog and Skolem Machines technical notes, spring 2007 1 The Geolog Language

    John Fisher; Marc Bezem
    Geolog is a language for expressing first-order geometric logic in a format suitable for computations using an abstract machine. Geolog rules are used as machine instructions for an abstract machine that computes consequences for first-order geometric logic. A Geolog rule has the general form A1, A2,..., Am ⇒ C1; C2;...; Cn where the Ai are atomic expressions and each Cj is a conjunction of atomic expressions, m, n ≥ 1. The left-hand side of a rule is called the antecedent of the rule (a conjunction) and the right- hand side is called the consequent (a disjunction). All atomic expressions can...

  6. A quantified logic of evidence

    Melvin Fitting
    A propositional logic of explicit proofs, LP, was introduced in [2], completing a project begun long ago by Gödel, [13]. In fact, LP can be looked at in a more general way, as a logic of explicit evidence, and there have been several papers along these lines. A major result about LP is the Realization Theorem, that says any theorem of S4 can be converted into a theorem of LP by some replacement of necessitation symbols with explicit proof terms. Thus the necessitation operator of S4 can be seen as a kind of implicit existential quantifier: there exists a proof...

  7. An Overview of Parallel Strategies for Transitive Closure on Algebraic Machines

    Stefano Ceri; Maurice A. W. Houtsma
    An important feature of database t chnology of the nineties i the use of distributed compu-tation for speeding up the xecution of complex queries. Today, the use of parallelism is tested in several experimental database architectures and a few commercial systems for conventional select-project-join queries. In particular, hash-based fragmentation is used to distribute data to disks under the control of different processors, in multi-processor architectures without shared memory, in order to perform selections a d joins in parallel. With the development of new (logic) query languages and deductive databases, the new dimension of recurslon has been added to query processing....

  8. On Eliminating Disjunctions in Stable Logic Programming

    Thomas Eiter; Michael Fink; Hans Tompits; Stefan Woltran
    Disjunction is generally considered to add expressive power to logic programs under the stable model semantics, which have become a popular programming paradigm for knowledge representation and reasoning. However, disjunction is often not really needed, in that an equivalent program without disjunction can be given. In this paper, we consider the question, given a disjunctive logic program, P, under which conditions an equivalent normal (i.e., disjunction-free) logic program P ′ exists. In fact, we study this problem under different notions of equivalence, viz. for ordinary equivalence (considering the collections of all stable models of the programs) as well as for...

  9. Hypothetical reasoning and definitional reflection in logic programming

    Peter Schroeder-heister
    This paper describes the logical and philosophical background of an extension of logic programming which uses a general schema for introducing assumptions and thus presents a new view of hypothetical reasoning. The detailed proof theory of this system is given in [7], matters of implementation and control of the corresponding programming language GCLA with detailed examples can be found in [1, 2]. In Section 1 we consider the local rule-based approach to a notion of atomic consequence as opposed to the global logical approach. Section 2 describes our system and characterises the inference schema of definitional reflection which is central...

  10. Using Social Network-based Trust For Default Reasoning On The Web

    Yarden Katz A; Jennifer Golbeck A
    A drawback of traditional default logic is that there is no general mechanism for preferring one default rule over another. To remedy this problem, numerous default logics augmented with priority relations have been introduced. In this paper, we show how trust values, derived from web-based social networks, can be used to prioritize defaults. We provide a coupling between the method for computing trust values in social networks and the prioritized Reiter defaults of (1), where specificity of terminological concepts is used to prioritize defaults. We compare our approach with specificity-based prioritization, and discuss how the two can be combined. Finally,...

  11. Synthesis of Irregular Combinational Functions with Large Don’t Care Sets

    V. Gherman; H. -j. Wunderlich; R. Mascarenhas
    A special logic synthesis problem is considered for Boolean functions which have large don’t care sets and are irregular. Here, a function is considered as irregular if the input assignments mapped to specified values (‘1 ’ or ‘0’) are randomly spread over the definition space. Such functions can be encountered in the field of design for test. The proposed method uses ordered BDDs for logic manipulations and generates free BDD-like covers. For the considered benchmark functions, implementations were found with a significant reduction of the node/gate count as compared to SIS or to methods offered by a state-of-the-art BDD package.

  12. Handling Exceptions in Nonmonotonic Reasoning

    Marcelino C. Pequeno; Rodrigo De M. S. Veras; Wladimir A. Tavares
    Abstract We introduce some differences in the style defeasible information is represented and inferences are made in nonmonotonic reasoning. These, at first sight harmless, changes, in fact, helped us to discover a very important principle guiding how inferences should be drawn in nonmonotonic reasoning, we name it the exception-first principle or EFP. DLEF is our own variant for default logic complying with EFP. We also show alternative definitions for Reiter’s default logics and its justified and constrained variants within our framework. DLEF does not produce anomalous extensions where the other default logics do. Restricted to the language of general logic...

  13. Gödel-Dummett Predicate Logics and Axioms of Prenexability

    Vítězslav ˇ Svejdar; R. Honzík; The Logica Yearbook
    Gödel-Dummett logic in general is a multi-valued logic where a truth value of a formula can be any number from the real interval [0, 1] and where implication → is evaluated via the Gödel implication function. As to truth values, 0 (falsity) and 1 (truth) are the extremal truth values whereas the remaining

  14. Reflection and Strategies in Rewriting Logic

    Manuel Clavel
    After giving general metalogical axioms characterizing reflection in general logics in terms of the notion of a universal theory , this paper specifies a finitely presented universal theory for rewriting logic and gives a detailed proof of the claim made in [5] that rewriting logic is reflective. The paper also gives general axioms for the notion of a strategy language internal to a given logic. Exploiting the fact that rewriting logic is reflexive, a general method for defining internal strategy languages for it and proving their correctness is proposed and is illustrated with an example. The Maude language has been...

  15. Detecting and Repairing Anomalous Evolutions in Noisy Environments: Logic Programming Formalization and Complexity Results

    Fabrizio Angiulli; Gianluigi Greco; Luigi Palopoli
    Summary. In systems where agents are required to interact with a partially known and dy-namic world, sensors can be used to obtain further knowledge about the environment. How-ever, sensors may be unreliable, that is, they may deliver wrong information (due, e.g., to hardware or software malfunctioning) and, consequently, they may cause agents to take wrong decisions, which is a scenario that should be avoided. The paper considers the problem of rea-soning in noisy environments in a setting where no (either certain or probabilistic) data is available in advance about the reliability of sensors. Therefore, assuming that each agent is equipped...

  16. Intention recognition with evolution prospection and causal Bayesian networks

    Lúıs Moniz Pereira; Han The Anh; Centro De Inteligência Artificial (centria
    Abstract. We describe a novel approach to tackle intention recognition, by combining dynamically configurable and situation-sensitive Causal Bayes Networks plus plan generation techniques. Given some situation, such networks enable the recognizing agent to come up with the most likely intentions of the intending agent, i.e. solve one main issue of intention recognition. And, in case of having to make a quick decision, focus on the most important ones. Furthermore, the combination with plan generation provides a signicant method to guide the recognition process with respect to hidden actions and unobservable effects, in order to confirm or disconfirm likely inten-tions. The...

  17. Closure on Algebraic Mach ines *

    Stefano Ceri; Maurice A. W. Houtsma
    An important feature of database t chnology of the nineties i the use of distributed compu-tation for speeding up the xecution of complex queries. Today, the use of parallelism is tested in several experimental database architectures and a few commercial systems for conventional select-project-join queries. In particular, hash-based fragmentation is used to distribute data to disks under the control of different processors, in multi-processor architectures without shared memory, in order to perform selections a d joins in parallel. With the development of new (logic) query languages and deductive databases, the new dimension of recurslon has been added to query processing....

  18. International Governance as New Raison d’État? The Case of the EU Common Foreign and Security Policy

    Mathias Koenig-archibugi
    Various scholars have suggested that at times national governments use international cooperation to gain influence in the domestic political arena and to overcome internal opposition to their preferred policies. Klaus Dieter Wolf has argued that this practice represents the latest embodiment of a longstanding raison d’état and has provided theoret-ical foundations for its systematic study. This article assesses the usefulness of this ‘new raison d’état ’ thesis as a source of empirical hypotheses about the origins and persistence of international institu-tions. On the basis of the general logic of the argument, I develop one crucial implication that may be corroborated...

  19. Expressing and Detecting Control Flow Properties of Distributed Computations

    Garg, Vijay,; Tomlinson, Alex; Fromentin, Eddy; Raynal, Michel
    Properties of distributed computations can be either on their global states or on their control flows. This paper addresses control flow properties. It first presents a simple yet powerful logic for expressing general properties on control flows, seen as sequences of local states. Among other properties, we can express invariance, sequential properties (to satisfy such a property a control flow must match a pattern described as a word on some alphabet) and non-sequential properties (these properties are on several control flows at the same time). A decentralized detection algorithm for properties described by this logic is then presented. This algorithm,...

  20. Encoding a dependent-type -calculus in a logic programming language

    Felty, Amy; Miller, Dale
    Various forms of typed l-calculi have been proposed as specification languages for representing wide varieties of object logics. The logical framework, LF is an example of such a dependent-type l-calculus. A small subset of intuitionistic logic with quantification over simply typed l-calculus has also been proposed as a framework for specifying general logics. The logic of hereditary Harrop formulas with quantification at all non-predicate types, denoted here as hhw is such a meta-logic that has been implemented in both the Isabelle theorem prover and the lProlog logic programming language. In this paper, we show how LF can be encoded into...

Aviso de cookies: Usamos cookies propias y de terceros para mejorar nuestros servicios, para análisis estadístico y para mostrarle publicidad. Si continua navegando consideramos que acepta su uso en los términos establecidos en la Política de cookies.