اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدProviding Hints, Next Steps and Feedback in a Tutoring System for Structural Induction
42
0
0.0
(
0
)
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
Structural induction is a proof technique that is widely used to prove statements about discrete structures. Students find it hard to construct inductive proofs, and when learning to construct such proofs, receiving feedback is important. In this paper we discuss the design of a tutoring system, LogInd, that helps students with constructing stepwise inductive proofs by providing hints, next steps and feedback. As far as we know, this is the first tutoring system for structural induction with this functionality. We explain how we use a strategy to construct proofs for a restricted class of problems. This strategy can also be used to complete partial student solutions, and hence to provide hints or next steps. We use constraints to provide feedback. A pilot evaluation with a small group of students shows that LogInd indeed can give hints and next steps in almost all cases.
قيم البحث
اقرأ أيضاً
We review the importance of recent UV observations of solar system targets and discuss the need for further measurements, instrumentation and laboratory work in the coming decade. In the past decade, numerous important advances have been made in so
lar system science using ultraviolet (UV) spectroscopic techniques. Formerly used nearly exclusively for studies of giant planet atmospheres, planetary exospheres and cometary emissions, UV imaging spectroscopy has recently been more widely applied. The geyser-like plume at Saturns moon Enceladus was discovered in part as a result of UV stellar occultation observations, and this technique was used to characterize the plume and jets during the entire Cassini mission. Evidence for a similar style of activity has been found at Jupiters moon Europa using Hubble Space Telescope (HST) UV emission and absorption imaging. At other moons and small bodies throughout the solar system, UV spectroscopy has been utilized to search for activity, probe surface composition, and delineate space weathering effects; UV photometric studies have been used to uncover regolith structure. Insights from UV imaging spectroscopy of solar system surfaces have been gained largely in the last 1-2 decades, including studies of surface composition, space weathering effects (e.g. radiolytic products) and volatiles on asteroids (e.g. [2][39][48][76][84]), the Moon (e.g. [30][46][49]), comet nuclei (e.g. [85]) and icy satellites (e.g. [38][41-44][45][47][65]). The UV is sensitive to some species, minor contaminants and grain sizes often not detected in other spectral regimes. In the coming decade, HST observations will likely come to an end. New infrastructure to bolster future UV studies is critically needed. These needs include both developmental work to help improve future UV observations and laboratory work to help interpret spacecraft data. UV instrumentation will be a critical tool on missions to a variety of targets in the coming decade, especially for the rapidly expanding application of UV reflectance investigations of atmosphereless bodies.
In the theory of coalgebras, trace semantics can be defined in various distinct ways, including through algebraic logics, the Kleisli category of a monad or its Eilenberg-Moore category. This paper elaborates two new unifying ideas: 1) coalgebraic tr
ace semantics is naturally presented in terms of corecursive algebras, and 2) all three approaches arise as instances of the same abstract setting. Our perspective puts the different approaches under a common roof, and allows to derive conditions under which some of them coincide.
Higher inductive-inductive types (HIITs) generalize inductive types of dependent type theories in two ways. On the one hand they allow the simultaneous definition of multiple sorts that can be indexed over each other. On the other hand they support e
quality constructors, thus generalizing higher inductive types of homotopy type theory. Examples that make use of both features are the Cauchy real numbers and the well-typed syntax of type theory where conversion rules are given as equality constructors. In this paper we propose a general definition of HIITs using a small type theory, named the theory of signatures. A context in this theory encodes a HIIT by listing the constructors. We also compute notions of induction and recursion for HIITs, by using variants of syntactic logical relation translations. Building full categorical semantics and constructing initial algebras is left for future work. The theory of HIIT signatures was formalised in Agda together with the syntactic translations. We also provide a Haskell implementation, which takes signatures as input and outputs translation results as valid Agda code.
User defined recursive types are a fundamental feature of modern functional programming languages like Haskell, Clean, and the ML family of languages. Properties of programs defined by recursion on the structure of recursive types are generally prove
d by structural induction on the type. It is well known in the theorem proving community how to generate structural induction principles from data type declarations. These methods deserve to be better know in the functional programming community. Existing functional programming textbooks gloss over this material. And yet, if functional programmers do not know how to write down the structural induction principle for a new type - how are they supposed to reason about it? In this paper we describe an algorithm to generate structural induction principles from data type declarations. We also discuss how these methods are taught in the functional programming course at the University of Wyoming. A Haskell implementation of the algorithm is included in an appendix.
The principle of strong induction, also known as k-induction is one of the first techniques for unbounded SAT-based Model Checking (SMC). While elegant and simple to apply, properties as such are rarely k-inductive and when they can be strengthened,
there is no effective strategy to guess the depth of induction. It has been mostly displaced by techniques that compute inductive strengthenings based on interpolation and property directed reachability (Pdr). In this paper, we present kAvy, an SMC algorithm that effectively uses k-induction to guide interpolation and Pdr-style inductive generalization. Unlike pure k-induction, kAvy uses Pdr-style generalization to compute and strengthen an inductive trace. Unlike pure Pdr, kAvy uses relative k-induction to construct an inductive invariant. The depth of induction is adjusted dynamically by minimizing a proof of unsatisfiability. We have implemented kAvy within the Avy Model Checker and evaluated it on HWMCC instances. Our results show that kAvy is more effective than both Avy and Pdr, and that using k-induction leads to faster running time and solving more instances. Further, on a class of benchmarks, called shift, kAvy is orders of magnitude faster than Avy, Pdr and k-induction.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
