Timing diagrams are popular in hardware design. They have been formalized for use in reasoning tasks, such as computer-aided verification. These efforts have largely treated timing diagrams as interfaces to established notations for which verification is decidable; this has restricted timing diagrams to expressing only regular language properties. This paper presents a timing diagram logic capable of expressing certain context-free and context-sensitive properties. It shows that verification is decidable for properties expressible in this logic. More (...) specifically, it shows that containment of -regular languages generated by Büchi automata in timing diagram languages is decidable. The result relies on a correlation between timing diagram and reversal bounded counter machine languages. (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.

We present a framework for verifying systems composed of heterogeneous reasoning agents, in which each agent may have differing knowledge and inferential capabilities, and where the resources each agent is prepared to commit to a goal (time, memory and communication bandwidth) are bounded. The framework allows us to investigate, for example, whether a goal can be achieved if a particular agent, perhaps possessing key information or inferential capabilities, is unable (or unwilling) to contribute more than a given portion of its (...) available computational resources or bandwidth to the problem. We present a novel temporal epistemic logic, BMCL-CTL , which allows us to describe a set of reasoning agents with bounds on time, memory and the number of messages they can exchange. The bounds on memory and communication are expressed as axioms in the logic. As an example, we show how to axiomatise a system of agents which reason using resolution and prove that the resulting logic is sound and complete. We then show how to encode a simple system of reasoning agents specified in BMCL-CTL in the description language of the Mocha model checker (Alur et al., Proceedings of the tenth international conference on computer-aided verification (CAV) , 1998), and verify that the agents can achieve a goal only if they are prepared to commit certain time, memory and communication resources. (shrink)

There is a long tradition of fruitful interaction between logic and social choice theory. In recent years, much of this interaction has focused on computer-aided methods such as SAT solving and interactive theorem proving. In this paper, we report on the development of a framework for formalizing voting theory in the Lean theorem prover, which we have applied to verify properties of a recently studied voting method. While previous applications of interactive theorem proving to social choice have focused (...) on the verification of impossibility theorems, we aim to cover a variety of results ranging from impossibility theorems to the verification of properties of specific voting methods. In order to formalize voting theoretic axioms concerning adding or removing candidates and voters, we work in a variable-election setting whose formalization makes use of dependent types in Lean. (shrink)

This paper is in two parts. Part I outlines three traditional approaches to the teaching of critical thinking: the normative, cognitive psychology, and educational approaches. Each of these approaches is discussed in relation to the influences of various methods of critical thinking instruction. The paper contrasts these approaches with what I call the “visualisation” approach. This approach is explained with reference to computer-aided argument mapping (CAAM) which uses dedicated computer software to represent inferences between premise and conclusions. (...) The paper presents a detailed account of the CAAM methodology, and theoretical justification for its use, illustrating this with the argument mapping software Rationale™. A number of Rationale™ design conventions and logical principles are outlined including the principle of abstraction, the MECE principle, and the “Holding Hands” and “Rabbit Rule” heuristics. Part II of this paper outlines the growing empirical evidence for the effectiveness of CAAM as a method of teaching critical thinking. (shrink)

Sometimes in the course of image-making, images are asked to represent unusual things. Around 1960, scientists and engineers working on the Computer-Aided Design Project at MIT began imagining that computers could be “active partners” to human designers. They began talking about a future of “human-computer symbiosis.” And they created a new type of image—the screenshot—that represented this new possibility. This paper describes early CAD research as a site for the emergence of the ideal of the interactive (...) class='Hi'>computer and how this ideal was described and distributed through screenshots.Though we now routinely associate computers with interactivity, interactivity was beyond the average user’s experience in 1960.... (shrink)

In the paper, we tackle the matter of non-classical logics, in particular, paraconsistent ones, for which not every formula follows in general from inconsistent premisses. Our benchmark is Jaśkowski’s logic, modeled with the help of discussion. The second key origin of this paper is the matter of being tabular, i.e. being adequately expressible by finitely many finite matrices. We analyse Jaśkowski’s non-tabular discussive (discursive) logic $ \textbf {D}_{2}$, one of the first paraconsistent logics, from the perspective of a trivalent tabular (...) logic. We are motivated to step down from the ongoing modal $ \textbf {S5}$-perspective of developing $ \textbf {D}_{2}$ both by certain mysteries that have been surrounding it and by gaps in Jaśkowski’s arguments contra the multivalent tabular perspective. Although Jaśkowski’s idea to use $ \textbf {S5}$ in order to define $ \textbf {D}_{2}$ is very attractive since it allows one to benefit from the tools and results of modal logic, it also gives a ‘non-direct’ formulation and, as it appeared later, is superfluous with respect to what is meant to be achieved since one can define the very same logic but using modal logics weaker than S5. It is also known, due to Kotas, that discussive logic is not finite-valued. So, in light of Kotas’s result that $ \textbf {D}_{2}$ is non-tabular, we propose to associate it with a few dozen discussive formulae that Jaśkowski unequivocally and illustratively suggests to be its theorems or non-theorems rather than with axioms of its modern axiomatizations (one of which Kotas employs) in order to be capable of performing a computer-aided brute-force search for suitable trivalent matrices in the cases of one and two designated values. As a result, we find trivalent matrices with two designated values that might be dubbed ‘discussive’ because they meet Jaśkowski’s suggestion to validate and invalidate the litmus theorems and non-theorems, respectively, despite the fact that none of them validates all the negation axioms in the modern axiomatizations of $ \textbf {D}_{2}$. The matrices found are then analysed along with highlighting the ones that were previously mentioned in the literature. We conclude the paper with a comparative analysis of Omori’s results and a test of Karpenko’s hypothesis. (shrink)

There are at least two reasons for the wide spread of CAI: 1. that the student is able to control his own process of learning due to immediate evaluation of his work and progress and 2. that evaluation is homogeneous, i.e. independent of subjective fac- tors, which compensates for possible lack of depth. Also, the psychology of man is such that he is less ashamed to be reprimanded for his errors by a machine than by another human being. It is (...) a specic feature of computer aided instruction of logic, particulary the art of proving, that such a system cannot be made other than open. Fortunately, in the case of logic its language makes such a creation possible. An open system is a system that permits arbitrary proof of theorems as long as the former conform to the requirement of a given formal language. The discussed system, Mizar-MSE, evolved, roughly speaking, the above line of thought. It is a natural deduction system practically applied to student instruction. Here I would like to present some of more specic features. (shrink)

This paper describes COMET, the first 'expert' computer system to incorporate a comprehensive set of the rules of law and medical ethics relating to consent to medical treatment.

The purpose is to improve the teaching and learning efficiency of college Innovation and Entrepreneurship Education. Firstly, from the perspective of aesthetic education, this work designs the teacher and student sides of the Computer-aided Instruction system. Secondly, the CAI model is implemented based on the weight sharing and local perception of the Convolutional Neural Network. Finally, the performance of the CNN-based CAI model is tested. Meanwhile, it analyses students’ IEE experience under the proposed CAI model through a case (...) study of Music Majors from Xi’an Conservatory of Music. The experimental data show that the CNN-based CAI model can respond quickly and stably when users access different functional modules, such as webpage browsing. The proposed CAI model increases students’ entrepreneurial interest, skills, and knowledge by 55.62, 57.32, and 72.12%, respectively. Students’ entrepreneurial practice ability has been improved by over 50.00%; such an increase in entrepreneurial practice ability has also shown individual differences. Thus, the proposed Music Majors-oriented IEE-infiltrated CAI model based on CNN improves students’ entrepreneurial practice ability and reflects the positive experience of Music Majors on IEE. The finding provides references for the step-by-step identification of the CNN-based CAI model and has certain guiding significance for analyzing the effect of college IEE. (shrink)

In this work, a system for the classification of liver dynamic contest- enhanced CT images is presented. The system simultaneously analyzes the images with the same slice location, corresponding to three typical acquisition moments. At first, the texture features are extracted separately for each acquisition mo- ment. Afterwards, they are united in one “multiphase” vector, characterizing a triplet of textures. The work focuses on finding the most appropriate features that characterize a multi-image texture. At the beginning, the features which are (...) unstable and dependent on ROI size are eliminated. Then, a small subset of remaining features is selected in order to guarantee the best possible classification accuracy. In total, 9 extraction methods were used, and 61 features were calculated for each of three acquisition moments. 1511 texture triplets, corresponding to 4 hepatic tissue classes were recognized. As a classifier, an adaptive boosting algorithm with a C4.5 tree was used. Experiments show that a small set of 12 features is able to ensure classification accuracy exceeding 90%, while all of the 183 features provide an accuracy rate of 88.94%. (shrink)

In the 1980s, computer-aided experimental research became standard in the majority of leading research laboratories. Unfortunately, this shift was not adequately reflected in the professional literature related to the philosophy and methodology of science. A new experimentalism did emerge, aimed at adequately describing experimental practice (to be discussed in the first part of this article); however, in its initial phase, it failed to consider the role of computers in experimental research (discussed in the second part). This oversight by (...) the philosophers of science, the proponents of the new experimentalism, is significant and calls for supplementation (addressed in the fourth part). By the turn of the 20 th and 21 st centuries, there were numerous philosophical analyses related to computer experiments, such as computer simulations. However, this article focuses only on classic experiments facilitated by various computer systems (e.g., LHC at CERN). In the final part of this article, I will present examples of aspects of experimental work that have not yet been analyzed and could potentially enhance new experimentalism with insights from computer-aided experiments. (shrink)

The present article examines the potential effects on the translation process of working interactively with a translation memory system, a tool for storing and sharing previous translations. A TM system automatically divides the source text into sentences presented to the translator one-by-one. Based on observations made in an empirical study of six professional translators and six translation students, it is argued that full sentences do not constitute a central cognitive processing category in translation, and that the sentence-by-sentence presentation inherent in (...) TM systems therefore creates an unnaturally strong focus on the sentence, which affects the very task of translation. Particular attention is given to the impact of the use of TM systems on the informants’ revision behaviour and their tendency to change the sentence structure. (shrink)

Part I of this paper outlined the three standard approaches to the teaching of critical thinking: the normative (or philosophical), cognitive psychology, and educational taxonomy approaches. The paper contrasted these with the visualisation approach; in particular, computer-aided argument mapping (CAAM), and presented a detailed account of the CAAM methodology and a theoretical justification for its use. This part develops further support for CAAM. A case is made that CAAM improves critical thinking because it minimises the cognitive burden of (...) prose and the demands that arguments in prose typically place on memory. CAAM also has greater usability, complements the imperfect human cognitive system, and adopts a logic of semi-formality which is both natural and intuitive. The paper claims that CAAM is an important advance given that traditional stand-alone critical thinking courses do not teach critical thinking as well as they as they are assumed to do. It is also important given that tertiary education fails to deliver improvements in critical thinking gains for too many students. The paper outlines results from a number of empirical studies that demonstrate that CAAM yields robust gains in critical thinking as measured by independent tests. Students themselves also believe CAAM to be beneficial as noted in coded responses to surveys. I conclude the paper by comparing the traditional approaches to the teaching of critical thinking to the visualisation approach. I argue that CAAM should taken seriously in the context of contemporary educational practices. (shrink)

This paper explores the application of an affective content analysis to a selection of nanotechnology news articles gathered from selected newspapers. Thematic content analyses dominate current efforts to mine large text collections of popular science media; the addition of an affective analysis element can yield useful information to supplement future content analysis efforts. Using Whissell’s Dictionary of Affect in Language , the analysis rates news articles gathered over a twenty-two year period for their pleasantness, activeness, and imagery, determining the mean (...) affective tone in each category for the entire collection, four ‘content themes’ (business, national security, health, and environment), and the change in affective tone over the twenty-two year period these articles represent. Whereas the entire collection analyzed as a whole rates very similarly to the average found for everyday English language use and the ‘content themes’ show similar results, the change in affective tone over the years has been both significant and striking. A sample of results from three years of the twenty-two year period is then qualitatively explored to demonstrate to the reader the connection between the quantitative results of the Dictionary and the qualitative effect of the article’s word use and phrasing. The paper ends with a review of the technique’s success, implications for policymaking and public dialogue, and avenues for future use. (shrink)

In recent years, with the development of construction industry, more scientific, systematic, fast, and intelligent calculation methods are needed to coordinate urban development and fierce market competition, and mathematical algorithm library plays an important role in artificial intelligence. Therefore, the author uses computer mathematical algorithm and extension theory to study and analyze the residential building design and intelligent data mining. It is found that the research of the computer-aided expression method of extension building planning is mainly the (...) expression of the input and output system of extension building planning. It includes knowledge representation, system outline design, system flow, and interface expression based on the mathematical database. (shrink)

In his Languages of Art, Nelson Goodman proposes a theory of artistic notation that includes foundational requirements for any system of symbols we might use to specify and communicate the features of an artwork, in architecture or any other art form. Goodmans' theory usefully explains how notation can reveal linguistic-like phenomena of various art forms. But not all art forms can enjoy benefits of a full-blown notational system, in Goodman's view, and he suggests that architecture's symbol systems fall short in (...) this regard. It is a shortcoming of architecture, he believes, that its notation cannot communicate the sum of a given work's essential features. Against this view it may be argued that artworks are generally and inimically historical in character, such that an inability to capture this dimension may result in a failure to pick out the identity of a work. As a consequence, the suggestion of that inability looks like a shortcoming of the general notational theory rather than of the art form or its notation per se. I defend Goodman's background formalism against the criticism that an ahistoricist notation cannot possibly be adequate. But I reject his view that no actual architectural notation can satisfy the formal criteria of his theory. In particular, I propose that the foundational theory for Computer Aided Design (CAD) described by the architect William Mitchell satisfies Goodman's criteria and so yields a notation that enables communication of an architectural work's essential features. If, as I suggest, such a notation is feasible, then we have an additional result that Goodman foresees: a means of abstracting future architectural works from their historical contexts. This in turn yields a consequence at which Goodman only hints-that such architectural works can be intellectually grasped and physically constructed along purely formalist lines. One practical result here is that we introduce economical solutions to architectural design. On a theoretical level, we also expose the inessential character of historical properties to creating or understanding architecture, at least with respect to future possible works. (shrink)

The acceptance or rejection of computer aids to clinical reasoning is determined not only by the preferences and prejudices of potential users, but also by whether the output generated by the computer aid represents sound clinical judgment. This paper deals with the issue of the appropriate criteria for evaluating the clinical ‘reasoning’ of computer aids. Evaluation of a computer aid should include an assessment of the accuracy or appropriateness of its conclusions and an assessment of the (...) scope of its considerations. In order to use a conclusion generated by a computer aid as a basis for clinical action, information must be available on the alternative conclusions that might have been drawn, the degree of confidence in each conclusion, and the consequences that may result from acting upon the wrong conclusion. If this information is not generated as part of the output of a computer aid, it may be obtained through the use of its explanation and display capabilities, if the aid has such capabilities. Explanation and display capabilities permit the examination of the operations of the computer aid. Examination of a computer's operations is also the most feasible means to evaluate the soundness of its ‘reasoning’. (shrink)

Profound changes in world markets are resulting in conflict between traditional structures of production and new market requirements. The right answers to this challenge are heavily disputed. One option is to replace human work still further by artificially intelligent technology without changing basic structures of production. In contrast to this strategy, alternative production concepts seek to combine the unique human capabilities of perception, evaluation and decision making in unstructured situations with appropriately designed computer systems. Empirical evidence from the use (...) of NC technology indicates that sensual experience and practical knowledge are necessary ingredients rather than disappearing residuals of efficient production. By far their tacit dimension does not allow complete transformation into objectified, scientific knowledge. In the field of metal cutting it is the skilled workers themselves who constitute the primary source of productivity. In order to overcome their traditionally problematic and uncomfortable working situation, shop-floor programming methods have been developed that are adapted to their concrete and graphic mode of thinking and acting. These allow workers to make their own efficient NC programs, thus maintaining their practical competence. This paper illustrates a necessary new perspective in system design: away from developing computer programs for imitating and replacing human expertise and towards designing computers as a useful tool for human experts. (shrink)

As individuals we often face complex issues about which we must weigh evidence and come to conclusions. Corporations also have to make decisions on the basis of strong and compelling arguments. Legal practitioners, compelled by arguments for or against a proposition and underpinned by the weight of evidence, are often required to make judgments that affect the lives of others. Medical doctors face similar decisions. Governments make purchasing decisions—for example, for expensive military equipment—or decisions in the areas of public or (...) foreign policy. These issues involve many arguments on all sides of difficult debates. These issues involve understanding the arguments of others and being able to make objections and provide rebuttals to objections. Students in universities deal with arguments all the time. A major purpose of a university education—regardless of subject matter—is to teach students how to read, understand, and respond to complex arguments. The ability to do this makes for highly employable, adaptable, and reflectively critical individuals. We often call the skill of marshaling arguments and assessing them “critical thinking.” All universities claim to instill the skill of critical thinking in their graduates and routinely note this in their advertising and promotional documents. This short paper outlines one way this skill can be taught. (shrink)

In 2014, the worldwide context is that the population is increasingly both expanding and aging in industrial countries. In contrast, the personal health levels of individuals could decrease. Although retirement homes and health-care centers assume most of the demand, they will most probably overflow in the next few years. One of the current solutions is e-Health, which involves biomedical monitoring but also home automation functions to compensate for disabilities that tend to increase with age. In this context, several domains have (...) to be merged while respecting the entire ecosystem: the users, their needs and environment, but also all the various actors/experts involved in this process. The issue, however, is that enormous effort is required to combine the multiple expert domains because these can be antinomic. Hence, this paper proposes a collaborative workflow that brings together these different actors and generates the control/command application. Applying model-driven engineering, this workflow makes a clear distinction between people’s health requirements, the home automation functions, and the user interface points of view. Thus, it allows experts in each field to adapt their system in terms of the user’s needs, disability, and health state. (shrink)

Pathological tremor is a common but highly complex movement disorder, affecting ~5% of population older than 65 years. Different methodologies have been proposed for its quantification. Nevertheless, the discrimination between Parkinson’s disease tremor and essential tremor remains a daunting clinical challenge, greatly impacting patient treatment and basic research. Here, we propose and compare several movement-based and electromyography-based tremor quantification metrics. For the latter, we identified individual motor unit discharge patterns from high-density surface electromyograms and characterized the neural drive to a (...) single muscle and how it relates to other affected muscles in 27 Parkinson’s disease and 27 essential tremor patients. We also computed several metrics from the literature. The most discriminative metrics were the symmetry of the neural drive to muscles, motor unit synchronization, and the mean log power of the tremor harmonics in movement recordings. Noteworthily, the first two most discriminative metrics were proposed in this study. We then used decision tree modelling to find the most discriminative combinations of individual metrics, which increased the accuracy of tremor type discrimination to 94%. In summary, the proposed neural drive-based metrics were the most accurate at discriminating and characterizing the two most common pathological tremor types. (shrink)

In this paper we summarize observations bridging the declared aspirations of pictorial semiotics and its real achievements. Pictorial semiotics is here understood as the general study of pictures as signs and it constituted a fundamental step beyond the art historical captivation with individual images. In the first part of our contribution we present a review of the most important methods that have been proposed as an answer to deal with several pictorial problems (multiple instances, segmentation, non-figurative meaning). In the second (...) part, we offer some positive and on-going implementations designed to remedy the shortcomings observed. What is suggested is the proof of concept that human researchers need the assistance of computing methodologies. However, computers can only do their job once an adequate phenomenology of human experience is fed into the process. (shrink)

Attempts to formalize the diagnostic process are by no means a recent undertaking; what is new is the availability of an engine to process these formalizations. The digital computer has therefore been increasingly turned to in the expectation of developing systems which will assist or replace the physician in diagnosis. Such efforts involve a number of assumptions regarding the nature of the diagnostic process: e.g. where it begins, and where it ends. ‘Diagnosis’ appears to include a number of quite (...) different cognitive processes, some of which seem more subject to formalization than others. Underlying the difficulties inherent in these efforts at formalization, is the hierarchical structure of medical knowledge including that of diseases. (By ‘hierarchical structure’, I mean no more than that our descriptions of clinical objects necessarily refer to different levels of organization; atomic, molecular, cellular, physiological system, entire patient.) Since diagnosis is in part a form of classification, measures of similarity between the clinical findings of a particular patient and a potential disease, are needed. This is complicated by the fact that some diseases are described using the vocabularies of physics and chemistry, others with the vocabulary of psychology, and most, with terms taken from a number of different hierarchical levels. The differences between the descriptions made using these vocabularies will be seen to exert systematic (if not uniform) influences upon the diagnostic process. CiteULike Connotea Del.icio.us What's this? (shrink)

One might poetically muse that computers have the essence both of logic and machines. Through the case of the history of Separation Logic, we explore how this assertion is more than idle poetry. Separation Logic works because it merges the software engineer’s conceptual model of a program’s manipulation of computer memory with the logical model that interprets what sentences in the logic are true, and because it has a proof theory which aids in the crucial problem of scaling the (...) reasoning task. Scalability is a central problem, and some would even say the central problem, in appli- cations of logic in computer science. Separation Logic is an interesting case because of its widespread success in verification tools. For these two senses of model—the engineering/conceptual and the logical—to merge in a genuine sense, each must maintain their norms of use from their home disciplines. When this occurs, both the logic and engineering benefit greatly. Seeking this intersection of two different senses of model provides a strategy for how computer scientists and logicians may be successful. Furthermore, the history of Separation Logic for analysing programs provides a novel case for philosophers of science of how software engineers and computer scientists develop models and the components of such models. We provide three contributions: an exploration of the extent of models merging that is necessary for success in computer science; an introduction to the technical details of Separation Logic, which can be used for reasoning about other exhaustible resources; and an introduction to the problems, process, and results of computer scientists for those outside the field. (shrink)

Peter Spirtes, Richard Scheines and Clark Glymour. Simulated Studies of the Reliability of Computer-Aided Model Specification Using the TETRAD, EQS and LISREL Programs.

Verification and validation of computer codes and models used in simulations are two aspects of the scientific practice of high importance that recently have been discussed widely by philosophers of science. While verification is predominantly associated with the correctness of the way a model is represented by a computer code or algorithm, validation more often refers to the model’s relation to the real world and its intended use. Because complex simulations are generally opaque to a practitioner, (...) the Duhem problem can arise with verification and validation due to their entanglement; such an entanglement makes it impossible to distinguish whether a coding error or the model’s general inadequacy to its target should be blamed in the case of a failure. I argue that a clear distinction between computer modeling and simulation has to be made to disentangle verification and validation. Drawing on that distinction, I suggest to associate modeling with verification and simulation, which shares common epistemic strategies with experimentation, with validation. To explain the reasons for their entanglement in practice, I propose a Weberian ideal–typical model of modeling and simulation as roles in practice. I examine an approach to mitigate the Duhem problem for verification and validation that is generally applicable in practice and is based on differences in epistemic strategies and scopes. Based on this analysis, I suggest two strategies to increase the reliability of simulation results, namely, avoiding alterations of verified models at the validation stage as well as performing simulations of the same target system using two or more different models. In response to Winsberg’s claim that verification and validation are entangled I argue that deploying the methodology proposed in this work it is possible to mitigate inseparability of V&V in many if not all domains where modeling and simulation are used. (shrink)