scholarly journals Mtac2: typed tactics for backward reasoning in Coq

2018 ◽  
Vol 2 (ICFP) ◽  
pp. 1-31 ◽  
Author(s):  
Jan-Oliver Kaiser ◽  
Beta Ziliani ◽  
Robbert Krebbers ◽  
Yann Régis-Gianas ◽  
Derek Dreyer
Keyword(s):  
2011 ◽  
Vol 121-126 ◽  
pp. 4481-4485
Author(s):  
Ai Yu Zhang ◽  
Xiao Guang Zhao ◽  
Lei Zhang

Due to the limited generality of traditional fault diagnosis expert system and its low accuracy of extracting failure symptoms, a general fault monitoring and diagnosis expert system has been built. For different devices, users can build fault trees in an interactive way and then the fault trees will be saved as expert knowledge. A variety of sensors are fixed to monitor the real-time condition of the device and intelligent algorithms such as wavelet transform and neural network are used to assist the extraction of failure symptoms. On the basis of integration of multi-sensor failure symptoms, the fault diagnosis is realized through forward and backward reasoning. The simulation diagnosis experiments of NC device have shown the effectiveness of the proposed method.


2019 ◽  
Vol 37 (5) ◽  
pp. 638-661 ◽  
Author(s):  
Abdul-Rasheed Amidu ◽  
David Boyd ◽  
Fernand Gobet

Purpose Behavioural studies of valuers have suggested that valuers rely on a number of cognitive strategies involving reasoning and intuition when undertaking a valuation task. However, there are few studies of the actual reasoning mechanisms in valuation. In other fields, much attention has been paid to forward and backward reasoning, as this shows the choices and decisions that are made in undertaking a complex task. This paper studied this during a valuation task. The purpose of this paper is twofold: first, to develop a methodological approach for empirical research on valuers’ reasoning, and, second, to report expert-novice differences on valuers’ use of forward and backward reasoning during a valuation problem solving. Design/methodology/approach The study utilised a verbal protocol analysis (VPA) to elicit think-aloud data from a purposive sample of a group of valuers of different levels of expertise undertaking a commercial-valuation task. Through a content analysis interpretive strategy, the transcripts were analysed into different cognitive segments identifying the forward and backward reasoning strategies. Findings The findings showed that valuers accomplished the valuation task by dividing the overall problem into sub-problems. These sub-problems are thereafter solved by integrating available data with existing knowledge by relying more on forward reasoning than backward reasoning. However, there were effects associated with the level of expertise in the way the processes of forward and backward reasoning are used, with the expert and intermediate valuers being more thorough and comprehensive in their reasoning process than the novices. Research limitations/implications This study explores the possibility that forward and backward reasoning play an important role in commercial valuation problem solving using a limited sample of valuers. Given this, data cannot be generalised to all valuation practice settings but may motivate future research that examines the effectiveness of forward and backward reasoning in diverse valuation practice settings and develops a holistic model of valuation reasoning. Practical implications The findings of this study are applicable to valuation practice. Future training efforts need to evaluate the usefulness of teaching problem solving and explicitly recognise forward and backward reasoning, along with other problem-solving strategies uncovered in this study, as standard training strategies for influencing the quality of valuation decisions. Originality/value By adopting VPA, this study employs an insightful and rich dataset which allows an interpretation of thoughts of valuers into cognitive reasoning strategies that provide a deeper level of understanding of how valuers solve valuation problem; this has not been possible in previous related valuation studies.


1995 ◽  
Vol 3 (4) ◽  
pp. 425-437 ◽  
Author(s):  
T. Arnould ◽  
S. Tano

Sign in / Sign up

Export Citation Format

Share Document