1. Features Using Logic Browser you can: - Logic Browser
The Logic Browser (Verilog only) is a compact, easy-to-read schematic window designed for analysis of complex designs. Drag a signal into the Logic Browser and click on ports to expand connectivity in relevant areas and build a multi-net schematic. Explore the design behavior by analyzing the annotated values for ports and nets as you go backwards and forwards in time. The Logic Browser dramatically simplifies debugging of bus collisions, tracing of undesired X values through complex circuitry, and understanding of design connectivity.

2. A Multiple-Conclusion Meta-Logic - A Multiple-conclusion Meta-logic,Dale Miller
The theory of cut-free sequent proofs has been used to motivate and justify the design of a number of logic programming languages. Two such languages, Prolog and its linear logic refinement, Lolli [12], provide for various forms of abstraction (modules, abstract data types, higher-order programming) but lack primitives for concurrency. The logic programming language, LO (Linear Objects) [2] provides for concurrency but lacks abstraction mechanisms. In this paper we present Forum, a logic programming presentation of all of linear logic that modularly extends the languages Prolog, Lolli, and LO. Forum, therefore, allows specifications to incorporate both abstractions and concurrency. As a meta-language, Forum greatly extends the expressiveness of these other logic programming languages. To illustrate...

3. A Logic for Object-Z - A Logic For Object-z,Graeme Smith
This paper presents a logic for Object-Z which extends W , the logic for Z adopted as the basis of the deductive system in the Z Base Standard. The logic provides a basis on which tool support for reasoning about Object-Z specifications can be developed. It also formalises the intended meaning of Object-Z constructs and hence provides an abstract, axiomatic semantics of the language. 1 Introduction Object-Z[10, 11, 7] is an extension of Z in which the existing syntax and semantics of Z are retained and new constructs are introduced to facilitate specification in an objectoriented style. The enhanced structuring improves the readability of large specifications. It also enables...

4. A Deterministic Terminating Sequent Calculus for Gödel-Dummett logic - Godel-dummett Logic
We give a short proof-theoretic treatment of a terminating contraction-free calculus G4-LC for the zero-order Godel-Dummett logic LC. This calculus is a slight variant of a calculus given by Avellone et al, who show its completeness by model-theoretic techniques. In our calculus, all the rules of G4-LC are invertible, thus allowing a deterministic proof-search procedure. Keywords: sequent calculus, contraction-free, terminating, Godel-Dummett logic 1 Introduction In previous work [9] the author gave a "contraction-free calculus" for zero-order intuitionistic logic IPL; following [21] we call this calculus G4ip. It has the property that root-first proof search terminates, thus allowing easy implementation without a loop-checker. See [9] for further history of this...

5. Free Variables and Subexpressions in Higher-Order Meta Logic - Meta Logic,Chuck Liang
This paper addresses the problem of how to represent free variables and subexpressions involving -bindings. The aim is to apply what is known as higher-order abstract syntax to higher-order term rewriting systems. Directly applying fi-reduction for the purpose of subtermreplacement is incompatible with the requirements of term-rewriting. A new meta-level representation of subterms is developed that will allow term-rewriting systems to be formulated in a higher-order meta logic.

6. Separation Logic for Higher-order Store - Hoare Logic
◮ partial correctness statements {p}c {q} ◮ command c ◮ pre-/post-condition assertions p, q about stores ◮ proof rules to derive valid triples ◮ fits nicely the model of while-languages with global store

7. Addendum to the paper "Belnap's four-valued logic and De Morgan lattices" - Four-valued Logic,De Morgan
the three above mentioned Gentzen systems are presented, together with the structural and multiple-conclusion versions and of GB and GBL , respectively. Then Theorem 4.88 of [7] states the same as Theorem 4.11 of [3], that is, the strong algebraizability of GB (denoted by in [7]), with the variety DM of De Morgan lattices as its equivalent algebraic semantics. And Theorem 4.98 of [7] states the non-algebraizability of , which is proved from the strong algebraizability of ; since it is obvious that the same fact and proof hold for their single-conclusion fragments, one can consider that this result also contains the non-algebraizability of GBL , which is the assertion in Theorem...

8. Two paradigms of logical computation in Affine Logic? - Affine Logic,G. Bellin,A Silvia Baraldini
We propose a notion of symmetric reduction for a system of proofnets for Multiplicative Affine Logic (MAL + MIX) (namely, multiplicative linear logic with unrestricted Weakening and Mix), related to the "cross-cut" reduction in classical logic LK. We prove that such a reduction has the strong normalization and the Church-Rosser properties. On one hand, the usual asymmetric cut elimination procedure in intuitionistic and linear logic is a form of "computation with garbage collection", and the cancellation of irrelevant parts is uniquely determined at any point of the process; such a paradigm can be applied to classical and affine logic through any one of the several known translations of classical logic...

9. Temporalizing Epistemic Default Logic - Temporalizing Epistemic,Default Logic,Temporalizing Epistemic Default,John-jules Meyer B
this paper in the Sections 2 to 6 the logic EDL is presented. As compared with earlier publications ([MH9 l a, MH92a, MH93a,b]), the logic is slightly extended in order to cater for downward reflection in subsequent sections. In Section 7 we define a labeled branching time temporalization of this logic, in spirit of the approach of [FG92]. In Section 8 we define sceptical and credulous entailment relations based on temporal models

10. $rec.titulo - Equational Propositional; Logic David Gries; Fred B. Schneider
Abstract We formalize equational propositional logic, prove that it is sound and complete, and compare the equational-proof style with the more traditional Hilbert style.

11. Verifying Probabilistic Programs Using A Hoare Like Logic - A Hoare Like Logic,J. I. Den Hartog,E. P. De Vink
Probability, be it inherent or explicitly introduced, has become an important issue in the verification of programs. In this paper we study a formalism which allows reasoning about programs which can act probabilistically. To describe probabilistic programs, a basic programming language with an operator for probabilistic choice is introduced and a denotational semantics is given for this language. To specify properties of probabilistic programs, standard first order logic predicates are insufficient, so a notion of probabilistic predicates is introduced. A Hoare-style proof system to check properties of probabilistic programs is given. The proof system for a sublanguage is shown to...

12. Higher-Order Equational Logic - Christian Prehofer,Tu Munchen,Contributions From Tobias Nipkow,C. Prehofer,Higher-order Equational Logic
Syntax" [Pfenning&Elliot 88] Applications: Programming languages, mathematics, formal systems ffl Higher-order theorem proving ffl Declarative Programming C. Prehofer, 6/97 Higher-Order Equational Logic 4 Declarative Programming Paradigms ? XXXXXXXXX Xz XXXXXXXXX Xz 9 9 ? Logic Programming Functional Programming Narrowing Higher-Order LP Higher-Order FP Higher-Order Narrowing C. Prehofer, 6/97 Higher-Order Equational Logic 5 Notation and Basic Definitions Variable Conventions ffl F; G; H;X;Y free variables ffl a; b; c; f; g (function) constants ffl x; y; z bound variables ffl ff; fi type variables ffl u,v,w constants or bound variables -terms: t = F j x j c j x:t j (t 1 t 2 ) Note: x n :s = x 1 : : : x n :s a(s n ) = ((Delta Delta Delta (a s 1 )...

13. Temporalizing Epistemic Default Logic - W. Van Der Hoek; W. Van Der Hoek; J. -j. Meyer; J. -j. Meyer; J. Treur; J. Treur; Temporalizing Epistemic Default
this paper in the Sections 2 to 6 the logic EDL is presented. As compared with earlier publications ([MH9 l a, MH92a, MH93a,b]), the logic is slightly extended in order to cater for downward reflection in subsequent sections. In Section 7 we define a labeled branching time temporalization of this logic, in spirit of the approach of [FG92]. In Section 8 we define sceptical and credulous entailment relations based on temporal models

14. Concepción de la polivalencia lógica en la Escuela de Varsovia - Domínguez Prieto, Pablo
Lukasiewilz -destacado miembro de la escuela de Luovvarsovia es considerado el fundador de la lógica polivalente. Se analiza en este trabajo la relación existente entre la doctrina de este lógico polaco con la de otros miembros de su misma escuela: Twardowski (fundador de ella y maestro de Lukasiervilz), Kotarbinski, Asdukiewierz Lesmienski (compañeros suyos. Y por último, Jaskowski y Zawirski (miembros de la segunda generación de la escuela de Luovvarsovia). En todos ellos, si bien no abundan doctrinas explícitas acerca de la polivalencia lógica, si son tratadas cuestiones de lógica, de filosofía del lenguaje o de filosofía de la ciencia fronteriza...

15. Reasoning About Set Constraints Applied to Tractable Inference in Intuitionistic Logic - Intuitionistic Logic,Thomas Drakengren,Peter Jonsson
Automated reasoning about sets has received a considerable amount of interest in the literature. Techniques for such reasoning have been used in, for instance, analyses of programming languages, terminological logics and spatial reasoning. In this paper, we identify a new class of set constraints where checking satisfiability is tractable (i.e. polynomial-time). We show how to use this tractability result for constructing a new tractable fragment of intuitionistic logic. Furthermore, we prove NP-completeness of several other cases of reasoning about sets. 215 1 Introduction There has been considerable interest in formalisms for describing and reasoning about sets. We begin by describing some of these. The most well-studied class of set constraints is, probably,...

16. La (lógica) contrucción de la realidad - Carrillo Guerrero, Lázaro
Every language activity requires some cognitive representations and some logic constructions in order to function upon the world and to get a position in the face of what is necessarily or probably truthful. In linguistic communication, this makes that the text be built according to some concrete and social logic alternatives, and that within each discourse there have an erected reality that is adaptable to the interlocutors and to the situations, and variable according to the participants' capacity and their strategic conjectures. In this frame, of social interaction and of language-thought relation, it is spread out an argumentative logic that...

17. An Operational Logic of Effects - Jacob Frost; Ian A. Mason
In this paper we describe our progress towards an operational implementation of a modern programming logic. The logic is inspired by the variable type systems of Feferman, and is designed for reasoning about imperative functional programs. The logic goes well beyond traditional programming logics, such as Hoare's logic and Dynamic logic in its expressibility, yet is less problematic to encode into higher-order logics. The main focus of the paper is too present an axiomatization of the base first-order theory, and an implementation of the logic into the generic proof assistant Isabelle. We also indicate the directions of our current research...

18. Low-power logic styles: CMOS versus pass-transistor logic - Reto Zimmermann; Wolfgang Fichtner
Abstract — Recently reported logic style comparisons based on full-adder circuits claimed complementary passtransistor logic (CPL) to be much more power-efficient than complementary CMOS. However, new comparisons performed on more efficient CMOS circuit realizations and a wider range of different logic cells, as well as the use of realistic circuit arrangementsdemonstrate CMOS to be superior to CPL in most cases with respect to speed, area, power dissipation, and power-delay products. An implemented 32-bit adder using complementary CMOS has a power-delay product of less than half that of the CPL version. Robustness with respect to voltage scaling and transistor sizing, as...

19. A Logic for Representing Grammatical Knowledge - Bill Keller
. Feature structures are partially specified, record-like structures which are employed in many recent grammar formalisms to represent linguistic objects of various kinds. Building on previous approaches to the logical representation of linguistic knowledge, this paper presents a logical language which is sufficiently expressive to allow for the encoding of recursive constraints on feature structures. A particular concern of this paper is to show how formulas of the logic can be used to capture the denotation of a grammar considered as a recursive definition of a class of linguistic objects. However, the logic may be of interest to researchers working...

20. A LOGIC PROGRAMMING EXTENSION FOR C CALLED CLOG - MARIA DO CARMO ELIAS ALVES
The use of declarative languages based in logic programming has been spread out due to the great interest in Artificial Intelligence. However, the use of these languages is not evident yet due to performance, portability, integration to other languages capability and other restrictions. This work contains the definition and implementation of a logic programming extension for C called Clog, which intends to cover the above deficiencies, allowing, mainly, the implementation of applications that have logic programming characteristics integrated to interative programming in the same development environment.

Página de resultados:
1  2  3  4  5  6  7  8  9  10  Siguiente