اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدStructural focalization
35
0
0.0
(
0
)
تأليف
Robert J. Simmons
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
Focusing, introduced by Jean-Marc Andreoli in the context of classical linear logic, defines a normal form for sequent calculus derivations that cuts down on the number of possible derivations by eagerly applying invertible rules and grouping sequences of non-invertible rules. A focused sequent calculus is defined relative to some non-focused sequent calculus; focalization is the property that every non-focused derivation can be transformed into a focused derivation. In this paper, we present a focused sequent calculus for propositional intuitionistic logic and prove the focalization property relative to a standard presentation of propositional intuitionistic logic. Compared to existing approaches, the proof is quite concise, depending only on the internal soundness and completeness of the focused logic. In turn, both of these properties can be established (and mechanically verified) by structural induction in the style of Pfennings structural cut elimination without the need for any tedious and repetitious invertibility lemmas. The proof of cut admissibility for the focused system, which establishes internal soundness, is not particularly novel. The proof of identity expansion, which establishes internal completeness, is a major contribution of this work.
قيم البحث
اقرأ أيضاً
Over the last 20 years a large number of automata-based specification theories have been proposed for modeling of discrete,real-time and probabilistic systems. We have observed a lot of shared algebraic structure between these formalisms. In this sho
rt abstract, we collect results of our work in progress on describing and systematizing the algebraic assumptions in specification theories.
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 pap
er 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.
The classical notions of structural controllability and structural observability are receiving increasing attention in Network Science, since they provide a mathematical basis to answer how the network structure of a dynamic system affects its contro
llability and observability properties. However, these two notions are formulated assuming systems with linear dynamics, which significantly limit their applicability. To overcome this limitation, here we introduce and fully characterize the notions structural accessibility and structural observability for systems with nonlinear dynamics. We show how nonlinearities make easier the problem of controlling and observing networked systems, reducing the number of variables that are necessary to directly control and directly measure. Our results contribute to understanding better the role that the network structure and nonlinearities play in our ability to control and observe complex dynamic systems.
We introduce several highness notions on degrees related to the problem of computing isomorphisms between structures, provided that isomorphisms exist. We consider variants along axes of uniformity, inclusion of negative information, and several othe
r problems related to computing isomorphisms. These other problems include Scott analysis (in the form of back-and-forth relations), jump hierarchies, and computing descending sequences in linear orders.
Gen Shirane began studying ferroelectrics while he was still based in Japan in the early 1950s. It was therefore natural that when he arrived at Brookhaven and began specialising in neutron scattering that he would devote much of his energy and exper
tise studying structural phase transitions. We review the ground breaking experiments that showed the behaviour of antiferroelectrics and ferroelectrics were reasonably described in terms of the soft mode concept of structural phase transitions. This work lead directly to Gen being awarded the Buckley prize and, jointly with John Axe, awarded the Warren prize. We then describe his work on incommensurate phase transitions and in particular how the giant Kohn anomalies are responsible for the structural instabilities in one-dimensional metals. Finally Gen carefully investigated the central peak and the two-length scale phenomena that occur at most if not all transitions. Due to Gens elegant experimental work we know a great deal about both of these effects but in neither case is theory able to explain all of his results
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
