In this paper I introduce a sequent system for the propositional modal logic S5. Derivations of valid sequents in the system are shown to correspond to proofs in a novel natural deduction system of circuit proofs (reminiscient of proofnets in linear logic, or multiple-conclusion calculi for classical logic). -/- The sequent derivations and proofnets are both simple extensions of sequents and proofnets for classical propositional logic, in which the new machinery—to take account of the modal vocabulary—is (...) directly motivated in terms of the simple, universal Kripke semantics for S5. The sequent system is cut-free and the circuit proofs are normalising. (shrink)

Short-circuit evaluation denotes the semantics of propositional connectives in which the second argument is evaluated only if the first is insufficient to determine the value of the expression. Com...

Short-circuit evaluation denotes the semantics of propositional connectives in which the second argument is evaluated only if the first argument does not suffice to determine the value of the expression. Free short-circuit logic is the equational logic in which compound statements are evaluated from left to right, while atomic evaluations are not memorised throughout the evaluation, i.e. evaluations of distinct occurrences of an atom in a compound statement may yield different truth values. We provide a simple semantics for (...) free short-circuit logic and an independent axiomatisation. Finally, we discuss evaluation strategies, some other SCLs, and side effects. (shrink)

We will be dealing with “sequential circuits” in the sense of E. F. Moore and G. H. Mealy. Each such circuit is assumed to have a finite number of input wires and a finite number of output wires. Each element of such a circuit will be assumed to be an and-circuit, an or-circuit, a not-circuit, or a delay circuit, for some specified temporal delay. Each element has one output wire which, however, may branch in order to serve several purposes (...) simultaneously. The and-circuits and or-circuits have two input wires each, while the not-circuits and the delay circuits have one input wire each. (shrink)

This book explains, in lay terms, the surprisingly simple system of mathematical logic used in digital computer circuitry. Anecdotal in its style and often funny, it follows the development of this logic system from its origins in Victorian England to its rediscovery in this century as the foundation of all modern computing machinery. ONES AND ZEROS will be enjoyed by anyone who has a general interest in science and technology.

Checking the equivalence of two Boolean functions, or combinational circuits modeled as Boolean functions, is often desired when reliable and correct hardware components are required. The most common approaches to equivalence checking are based on simulation and model checking, which are constrained due to the popular memory and state explosion problems. Furthermore, such tools are often not user-friendly, thereby making it tedious to check the equivalence of large formulas or circuits. An alternative is to use mathematical tools, called (...) interactive theorem provers, to prove the equivalence of two circuits; however, this requires human effort and expertise to write multiple output functions and carry out interactive proof of their equivalence. In this paper, we define two simple, one formal and the other informal, gate-level hardware description languages, design and develop a formal automatic combinational circuit equivalence checker tool, and test and evaluate our tool. The tool CoCEC is based on human-assisted theorem prover Coq, yet it checks the equivalence of circuit descriptions purely automatically through a human-friendly user interface. It either returns a machine-readable proof of circuits’ equivalence or a counterexample of their inequality. The interface enables users to enter or load two circuit descriptions written in an easy and natural style. It automatically proves, in few seconds, the equivalence of circuits with as many as 45 variables. CoCEC has a mathematical foundation, and it is reliable, quick, and easy to use. The tool is intended to be used by digital logic circuit designers, logicians, students, and faculty during the digital logic design course. (shrink)

The living mycelium networks are capable of efficient sensorial fusion over very large areas and distributed decision making. The information processing in the mycelium networks is implemented via propagation of electrical and chemical signals en pair with morphological changes in the mycelium structure. These information processing mechanisms are manifested in experimental laboratory findings that show that the mycelium networks exhibit rich dynamics of neuron-like spiking behaviour and a wide range of non-linear electrical properties. On an example of a single real (...) colony of _Aspergillus niger_, we demonstrate that the non-linear transformation of electrical signals and trains of extracellular voltage spikes can be used to implement logical gates and circuits. The approaches adopted include numerical modelling of excitation propagation on the mycelium network, representation of the mycelium network as a resistive and capacitive network and an experimental laboratory study on mining logical circuits in mycelium bound composites. (shrink)

We propose that, for the purpose of studying theoretical properties of the knowledge of an agent with Artificial General Intelligence (that is, the knowledge of an AGI), a pragmatic way to define such an agent’s knowledge (restricted to the language of Epistemic Arithmetic, or EA) is as follows. We declare an AGI to know an EA-statement φ if and only if that AGI would include φ in the resulting enumeration if that AGI were commanded: “Enumerate all the EA-sentences which you (...) know.” This definition is non-circular because an AGI, being capable of practical English communication, is capable of understanding the everyday English word “know” independently of how any philosopher formally defines knowledge; we elaborate further on the non-circularity of this circular-looking definition. This elegantly solves the problem that different AGIs may have different internal knowledge definitions and yet we want to study knowledge of AGIs in general, without having to study different AGIs separately just because they have separate internal knowledge definitions. Finally, we suggest how this definition of AGI knowledge can be used as a bridge which could allow the AGI research community to import certain abstract results about mechanical knowing agents from mathematical logic. (shrink)

This paper reviews three social scientific accounts of the civic sector's role in society: the government failure, contract failure, and voluntary failure theories. All three explain the role of nonprofit organizations as compensating for the market's failure to provide certain collective goods. This approach involves a radical misinterpretation of the underlying principles of civic sector organizations. An account is needed that explains their economy in terms of their normative concerns, rather than explaining normative concerns in terms of their economy. I (...) lay a foundation for such an account by examining the self-understanding among civic sector organizations that they should be "mission-driven," and the implications of this self-understanding for the sector as a "social economy." Whereas "mission-drivenness" calls attention to service-provision, resource-sharing, and open communication as the normative core of civic sector organizations, the notion of a "social economy" suggests a recirculation of money into channels where standard economic logic no longer holds. The key to the civic sector's role lies not in responses to market failure, but in the short-circuiting of a money-driven capitalist economy. (shrink)

A simplified model using kinetic logic is proposed to approach the problem after Hepatitis B viral (HBV) infection. It accounts for several stable regimes or attractors corresponding to the essential dynamic behaviour of the replication of the Hepatitis B virus. Infection with the virus can result in viral clearance, fulminant hepatic failure and death, or chronic transmissible infection, that is multistationarity corresponding to the existence of the positive feedback circuit in our modelling. Another implication of this model is the (...) existence of oscillations or homeostatic mechanisms, sometimes observed in the viral cycle, consistent with the existence of the negative feedback circuit. Thus, this report shows how a simple model of kinetic logic may be used to account for the variety of manifestations of HBV infection. This model implies the presence of the Hepatitis B e antigen, whose conservation suggests that it plays an important role in the life cycle of hepadnaviruses. Its function in the viral cycle is still unknown, but our model suggests that this antigen could explain the passage from one state of the viral infection (acute or latent) to another, as well as the oscillatory behavior which may account for the intermittent symptoms of hepatitis observed in some patients. Furthermore, this model shows a virgin state. This state is also reached after recovery. The model proposed demonstrates that starting from a viral acute infection, the host's immune response, depending on the immunological status of the patient, can lead to viral clearance, or to periodic spontaneous reactivation. (shrink)

Rice Combinational and Sequential Logic This text provides a guide to combinational and sequential logic, introducing students to the basic concepts then progressing to HND/first year undergraduate level. It has a highly practical emphasis, enabling the reader to simulate, build and test the circuits discussed in the text. Electronics Workbench files are provided for simulation, while easy-to-use XPLA software and specially designed hardware encourage the reader to build and test the circuits using programmable logic. The (...) text itself contains many self-assessment questions, complete with detailed answers, allowing students to test themselves as they learn. No previous experience of the topic is required and an abundance of practical examples helps students to apply the basic principles. The accompanying CD-ROM provides the XPLA development system software and Electronics Workbench files, as well as the Xilinx Webpack development system and 'walkthrough'. Hardware for Programmable Logic experiments can either be purchased or built following instructions from the text. Altogether, the text, software and hardware provide an interactive and stimulating teaching and learning resource. F. (shrink)

The value of logic techniques in circuit design has been well-known for many years, but a thorough grounding in mathematical logic is needed for all stages of software development, especially program specification, verification and program transformation. In all these stages, logic underpins the theory, bearing out the dictum that Logic is the calculus of computer science. This book presents the subject of mathematical logic in order to provide a grounding for students in computer science.

In this paper we relax the assumption that the logical constants of ordinary first-order logic be linearly ordered. As a consequence, we shall have formulas involving not only partially ordered quantifiers, but also partially ordered connectives. The resulting language, called the language of informational independence will be given an interpretation in terms of games of imperfect information. The II-logic will be seen to have some interesting properties: It is very natural to define in this logic two negations, (...) weak negation as failure to verify a sentence, and strong negation as the existence of a falsifying strategy: One can express in this logic complete problems of finite structures, like the non-connectedness and 3-colorability of finite graphs, the satisfiability problem for Boolean circuits built up from NAND-gates, etc. (shrink)

"Offering integrated coverage of both digital and computer design, this text offers well-organized, concise, yet comprehensive content, presented from a contemporary engineering viewpoint. Understanding of the material is supported by clear explanations and a progressive development of examples ranging from sample combinatorial applications to a CISC architecture built upon a RISC core. A thorough coverage of traditional topics is combined with increased attention to computer-aided design, problem formulation, solution verification, and the building of problem-solving skills."--BOOK JACKET.

Investigates how, given their ontological status between the One and animals, men can either ascend to the intellectual life or fall into the inferior kinds of life. Different issues involved in the doctrine of the rise to the intellectual life are considered. Firstly, the restriction to men of the possibility of an intellectual life is explained through the reference to Neoplatonists’ own personal experiences. Secondly, the experience of the ascent is defined by the term ‘inclination’ rather than the too broad (...) ‘reversion’ used by most of the scholars. The former term, indeed, seems to fit better in the case of men. Finally, the experience of inclination is explained in terms of logical necessity. (shrink)