No description available.

No description available.

We hypothesize and confirm that probabilistic reasoning is closely related to constraint satisfaction at a formal level, and that this relationship yields effective algorithms for guiding constraint satisfaction and constraint optimization solvers. By taking a unified view of probabilistic inference and constraint reasoning in terms of graphical models, we first associate a number of formalisms and techniques between the two areas. For instance, we characterize search and inference in constraint reasoning as summation and multiplication (or disjunction and conjunction) in the probabilistic space; necessary but insufficient consistency conditions for solutions to constraint problems (like arc-consistency) mirror approximate objective functions over probability distributions (like the Bethe free energy); and the polytope of feasible points for marginal probabilities represents the linear relaxation of a particular constraint satisfaction problem. While such insights synthesize an assortment of existing formalisms from varied research communities, they also yield an entirely novel set of “bias estimation” techniques that contribute to a growing body of research on applying probabilistic methods to constraint problems. In practical terms, these techniques estimate the percentage of solutions to a constraint satisfaction or optimization problem wherein a given variable is assigned a given value. By devising search methods that incorporate such information as heuristic guidance for variable and value ordering, we are able to outperform existing solvers on problems of interest from constraint satisfaction and constraint optimization–-as represented here by the SAT and MaxSAT problems. Further, for MaxSAT we present an equivalent transformation” process that normalizes the weights in constraint optimization problems, in order to encourage prunings of the search tree during branch-and-bound search. To control such computationally expensive processes, we determine promising situations for using them throughout the course of an individual search process. We accomplish this using a reinforcement learning-based control module that seeks a principled balance between the exploration of new strategies and the exploitation of existing experiences.

No description available.

This thesis is on the automation of diagrammatic proofs, a novel approach to mechanised mathematical reasoning. Theorems in automated theorem proving are usually proved by formal logical proofs. However, there are some conjectures which humans can prove by the use of geometric operations on diagrams that somehow represent these conjectures, so called diagrammatic proofs. Insight is often more clearly perceived in these diagrammatic proofs than in the algebraic proofs. We are investigating and automating such diagrammatic reasoning about mathematical theorems. Concrete rather than general diagrams are used to prove ground instances of a universally quantified theorem. The diagrammatic proof in constructed by applying geometric operations to the diagram. These operations are in the inference steps of the proof. A general schematic proof is extracted from the ground instances of a proof. it is represented as a recursive program that consists of a general number of applications of geometric operations. When gien a particular diagram, a schematic proof generates a proof for that diagram. To verify that the schematic proof produces a correct proof of the conjecture for each ground instance we check its correctness in a theory of diagrams. We use the constructive omega-rule and schematic proofs to make a translation from concrete instances to a general argument about the diagrammatic proof. The realisation of our ideas is a diagrammatic reasoning system DIAMOND. DIAMOND allows a user to interactively construct instances of a diagrammatic proof. It then automatically abstracts these into a general schematic proof and checks the correctness of this proof using an inductive theorem prover.

<p class="Abstract">The work proposed in this thesis continues the research into qualitative model learning (QML), a branch of qualitative reasoning.&nbsp; After the investigation of all existing qualitative model learning systems, especially the state-of-the-art system ILP-QSI, a novel system named QML-Morven is presented. <p class="Abstract">QML-Morven inherits many essential features of the existing QML systems: it can learn models from positive only data, make use of the well-posed model constraints, process hidden variables, learn models from incomplete data, and perform systematic experiments to verify the hypotheses being made by researchers. <p class="Abstract">The development of QML-Morven allows us to further investigate some interesting yet unsolved questions in the QML research.&nbsp; As a result, four significant hypotheses are tested and validated by performing a series of systematic experiments with QML-Morven:&nbsp; 1. The information of state variables and the number of hidden variables are two important actors that can influence the learning, and the different combination of these two factors may give a different learning result in terms of the kernel subset (minimal data for a successful learning) and learning precision; 2. The scalability of QML may be improved by the use of an evolutionary algorithm; 3. For some models, the kernel subsets can be constructed by combining several sets of qualitative states, and the states in a kernel subset tend to scatter over the solution space; 4. The integration of domain-specific knowledge makes QML more applicable for learning the qualitative models of the real-world dynamic systems of high complexity. <p class="Abstract">The results and analysis of these experiments with respect to QML-Morven also raise many questions and indicates several new research directions.&nbsp; In the final part of this thesis, several possible future directions are explored.

Theories of how individuals reason, and how they experience emotion abound in the psychological literature; yet, despite the common lay-theories of how emotions might affect a person’s reasoning, very little empirical work has been conducted on this relationship. The current thesis addresses this knowledge-gap by first distilling from the literature two classes of emotion theory; Information, and Load; and then systematically testing the explanatory power of these theories. A dual-process framework is employed in order to define low (Type One) and high effort (Type Two) strategies. Information theories predict that negative emotion cues more analytic processing relative to positive emotion, whereas load theories predict both positive and negative emotion to suppress use of high-effort strategies. Thus the two theories are compared by varying incidental and integral emotion across syllogistic reasoning, conditional reasoning, and the ratio-bias task, and assessing the engagement of Type One and Type Two processes across positive emotion, negative emotion, and control conditions. The findings suggest that emotion effects in syllogistic reasoning do not consistently support either Load or Information theories (Experiments 1-4). Emotion effects are found to be typically larger for integral than incidental emotion (Experiment 5), and most frequently serve as Information in verbal (Experiments 6 and 7) and visual conditional reasoning tasks (Experiment 8). Furthermore, these effects are to a large extent dependent on task properties such as the number of alternative antecedents (Experiments 9 and 10), and are greater on more difficult tasks (Experiments 11 and 12). These findings suggest that emotion has a greater impact on Type Two than Type One processes. A range of methodological and theoretical implications which will inform future work in this area are also discussed in the closing chapter.

by Yuen Siu Ming. / Thesis (M.Phil.)--Chinese University of Hong Kong, 1995. / Includes bibliographical references (leaves 104-110). / Chapter 1 --- Introduction --- p.1 / Chapter 2 --- Background --- p.4 / Chapter 2.1 --- Approaches in Formal Hardware Verification --- p.4 / Chapter 2.1.1 --- Theorem Proving --- p.5 / Chapter 2.1.2 --- Symbolic Simulation --- p.5 / Chapter 2.1.3 --- Model Checking --- p.6 / Chapter 2.2 --- Temporal Theories --- p.7 / Chapter 2.3 --- Related Works --- p.8 / Chapter 2.3.1 --- Consistency and Satisfiability of Timing Specifications --- p.8 / Chapter 2.3.2 --- Symbolic Constraint Satisfaction --- p.9 / Chapter 3 --- Problem Domain --- p.11 / Chapter 3.1 --- Basics of MC68000 Read Cycle --- p.11 / Chapter 4 --- Knowledge-based System Structure --- p.13 / Chapter 4.1 --- Diagnostic Reasoning Mechanisms --- p.14 / Chapter 4.2 --- Occurring Event Sequence --- p.16 / Chapter 4.3 --- Equivalent Goals --- p.17 / Chapter 4.4 --- CPU Databus Setup Time --- p.17 / Chapter 4.5 --- Assertion of CPU AS Signal --- p.19 / Chapter 5 --- Time Range Approach --- p.21 / Chapter 5.1 --- Time Range Represent ation --- p.21 / Chapter 5.2 --- Time Ranges Reasoning Techniques --- p.22 / Chapter 5.2.1 --- Constraint Satisfaction of Time Ranges --- p.22 / Chapter 5.2.2 --- Constraint Propagation of Time Ranges --- p.25 / Chapter 5.3 --- Worst-Case Timing Analysis --- p.28 / Chapter 5.4 --- System Implementation --- p.29 / Chapter 5.4.1 --- CPU Databus Setup Time --- p.30 / Chapter 5.4.2 --- Assertion of CPU AS Signal --- p.36 / Chapter 5.5 --- Implementation Results --- p.40 / Chapter 5.5.1 --- CPU Databus Setup Time --- p.40 / Chapter 5.5.2 --- Assertion of CPU AS Signal --- p.40 / Chapter 5.6 --- Conclusion --- p.41 / Chapter 6 --- Fuzzy Time Point Approach --- p.43 / Chapter 6.1 --- Fuzzy Time Point Models --- p.44 / Chapter 6.1.1 --- Concept of Fuzzy Numbers --- p.44 / Chapter 6.1.2 --- Definition of Fuzzy Time Points --- p.45 / Chapter 6.1.3 --- Semi-bounded Fuzzy Time Points --- p.47 / Chapter 6.2 --- Fuzzy Time Point Reasoning Techniques --- p.48 / Chapter 6.2.1 --- Constraint Propagation of Fuzzy Time Points --- p.50 / Chapter 6.2.2 --- Constraint Satisfaction of Fuzzy Time Points --- p.52 / Chapter 6.3 --- System Implementation --- p.55 / Chapter 6.3.1 --- Representation of Fuzzy Time Point --- p.55 / Chapter 6.3.2 --- Fuzzy Time Point Satisfaction --- p.56 / Chapter 6.3.3 --- Fuzzy Time Point Propagation --- p.58 / Chapter 6.4 --- Implementation Results --- p.64 / Chapter 6.4.1 --- CPU Databus Setup Time --- p.64 / Chapter 6.4.2 --- Assertion of CPU AS Signal --- p.65 / Chapter 6.5 --- Fuzzy Time Point Model Parameters --- p.66 / Chapter 6.5.1 --- Variation of Semi-bounded ftps' Membership Function --- p.66 / Chapter 6.5.2 --- Variation of μftp --- p.67 / Chapter 6.5.3 --- Variation of K --- p.69 / Chapter 6.6 --- Conclusion --- p.69 / Chapter 7 --- Constraint Compatibility Reasoning --- p.72 / Chapter 7.1 --- Abstract Timing Parameters --- p.73 / Chapter 7.2 --- MC68000 Read Cycle: Wait States Insertion --- p.75 / Chapter 7.3 --- Constraint Compatibility of Fuzzy Time Point --- p.75 / Chapter 7.3.1 --- Crisp Threshold Value --- p.77 / Chapter 7.3.2 --- Possibility Quantification for the Number of Wait States --- p.78 / Chapter 7.3.3 --- Threshold Beyond Fuzzy Time Point --- p.80 / Chapter 7.3.4 --- Fuzzy Time Point Beyond Threshold --- p.80 / Chapter 7.3.5 --- Threshold Within Fuzzy Time Point --- p.82 / Chapter 7.4 --- Determine When CPU Clock State is S5 --- p.83 / Chapter 7.5 --- System Implementation --- p.84 / Chapter 7.5.1 --- Expert's Heuristic Rule --- p.84 / Chapter 7.5.2 --- Constraint Compatibility --- p.85 / Chapter 7.5.3 --- Wait States Insertion --- p.87 / Chapter 7.6 --- Implementation Results --- p.91 / Chapter 7.7 --- Conclusion --- p.93 / Chapter 8 --- Conclusion --- p.95 / Chapter 8.1 --- Applications in Other Domains --- p.97 / Chapter 8.2 --- Future Directions and Recommendations --- p.98 / Chapter A --- Constraint Compatibility Reasoning Output --- p.99 / Chapter A.1 --- No Wait Cycle Insertion --- p.99 / Chapter A.2 --- Single Wait Cycle Insertion --- p.100 / Chapter A.3 --- Two Wait Cycle Insertions --- p.100 / Chapter B --- MC68020 Read Cycle Problem --- p.101 / Chapter B.1 --- Basics of MC68020 Read Cycle --- p.101 / Chapter B.2 --- MC68020 Databus Setup Time --- p.102 / Chapter B.3 --- Implementation Results --- p.103 / Bibliography --- p.104

The use of electroencephalography (EEG) to exam the electrical brain activity associated with reasoning provides an opportunity to quantify the functional and temporal aspects of this uniquely human capability, and at the same time expand our knowledge about what a given event-related potential (ERP) might measure. The question of what form of mental representation and transformational processes underlie human reasoning has been a central theme in cognitive psychology since its inception (Chomsky, 1957; McCarthy, 1955; Miller, 1956; Newell, Shaw, Simon, 1958). Two prominent, but competing views remain at the forefront of the discussion, one positing that human inference making is principally syntactic (Braine & O'Brien, 1998; Fodor, 1975; Pylyshyn, 1984; Rips, 1994), and the other that it is, fundamentally, semantic in nature (Gentner & Stevens, 1983; Johnson-Laird, 1983). The purpose of the proposed study is to investigate the neurophysiology of mental model (MM) and mental rule (MR) reasoning using high-density electroencephalography (EEG), with the goal of providing a characterization of the time course and a general estimate of the spatial dimensions of the brain activations correlated with these specific instances of two classic views of reasoning. The research is motivated by two questions: 1) Will violations of expectancy established by the devised MM and MR reasoning strategies evoke the N400 and P600 ERPs, respectively, and 2) Will topographical scalp distributions associated with each reasoning strategy suggest distinct psychological representations and processes? A finding of a N400 response in the MM condition suggests that reasoning about the relations between entities in the type of problems presented engages a network of cortical areas previously shown to be involved in processing violations of semantic expectancies in studies of language comprehension. By comparison, incongruent events in the MR condition are expected to evoke a bilateral anterior P600, a component previously associated with recognizing and restructuring syntactic anomalies or incongruities in sentence comprehension. If the hypothesized results are obtained they would provide potentially insightful information about the chronometry of mental processes associated with the different representations and inference making mechanisms postulated to support each mode of reasoning, and as well, broaden our understanding of the neural functionality associated with the N400 and P600 ERP.

In my dissertation, I advance and defend a broad account of reasoning, including both the nature of inference and the structure of our reasoning systems. With respect to inference, I argue that we have good reason to consider a unified account of the cognitive transitions through which we attempt to figure things out. This view turns out to be highly inflationary relative to previous philosophical accounts of inference, which, I argue, fail to accommodate many instances of everyday reasoning. I argue that a cognitive transition’s status as an inference, in this broad sense, depends on the subject’s taking the conclusion of the inference— a new, revised, or supposed belief— to be the output of a rational thought process. Furthermore, taking such a belief to be the output of a rational thought process consists in its accompaniment by the feeling of correctness to the subject, which I call the assent affect. With respect to the structure of our reasoning systems, I defend a dual process model of reasoning by addressing certain alleged deficiencies with such accounts. I argue that the assent affect— or more precisely its absence— is a strong candidate to serve as the triggering condition of our more deliberate type 2 reasoning processes. That is, a subject’s more effortful reasoning processes engage with a problem when the output of a type 1 intuition is not accompanied by the assent affect. A subject will think harder about a problem, in other words, when they do not feel confident that they have gotten to the bottom of it. This account, I argue, fits well with both empirical and theoretical claims about the interaction of dual reasoning processes. In this dissertation, I use the assent affect to solve puzzles about both the nature of inferences and the structure of our reasoning systems. Puzzles in rationality become easier to solve when our intellectual feelings are not excluded from the picture.