Tableau Workbook 1

The workbook contains everything up until the end of Tutorial 2. You can use it if you need to work through Tutorial 2 but don't have your saved file available from last week.

Le tableau numérique interactif: une intégration dans une communauté coopérative Freinet

Dans cette étude, nous nous sommes intéressé à l’utilisation des TIC, plus précisément du Tableau Numérique Interactif (TNI), en géométrie, par des groupes d’élèves de deux classes du primaire en pédagogie Freinet. S’inspirant d’une revue de littérature concernant la pédagogie dialogique, qui se rapproche de la pédagogie Freinet, trois unités d’observation, qui se rapportent aux trois types de discussion (cumulatif, disputationnel et exploratoire) au sein des groupes, ont été analysées. Le but de l’étude est de comprendre en quoi les discussions des groupes d’élèves autour du TNI, dans un contexte dit dialogique, peuvent être exploratoires (un type de discussion qui favoriserait les apprentissages). Pour cela, une activité d’apprentissage, appelée situation-problème, impliquant six groupes d’élèves autour du TNI, a été créée en collaboration avec les enseignants en géométrie. Nos résultats indiquent, entres autres, que les aspects pédagogiques de la technologie en question, ici le TNI, sont à différencier des aspects pédagogiques du logiciel utilisé, ici Tinkercad en mathématiques. Ce mémoire remet en relief toute la complexité de prendre en compte un unique facteur (l’analyse des discussions) pour discuter des apprentissages des élèves autour du TNI.

Les états de transformation dans une installation à partir de la matrice-tableau

Ce mémoire propose de retracer un parcours sur l’expérience du processus, mes essais en productions et en diffusion. Développé en trois parties, il décrit d’abord mes premières impressions perceptuelles des oeuvres, ensuite les différentes étapes qui auront ponctué ma recherche-création. Attentive à ce qui se passe en dehors des ateliers et des centres de diffusion en arts visuels, mes écrits sont teintés de mes expériences de diffusion et de création dans les lieux urbains et même, dans le dernier mois, dans le paysage naturel. J’explore mes méthodes de recherche-création instinctive et les différentes facettes entre les thèmes de la tension et de l’abandon. Je m’intéresse à la perception de ces mondes, à leurs cohabitations, à ce qu’ils produisent dans l’oeuvre finale et même, à l’expérience de mon propre corps. Je traiterai également du médium vidéo et de la valeur de l’image en comparaison aux autres médiums exploités, un ensemble d’oeuvres qui matérialisent une certaine temporalité de l’image en mouvement, où l’expérience à vivre est celle de l’instant suspendu ou une vision renouvelée du temps qui passe.

Une aide importante à la prise de décision : le tableau de bord pour administrateurs

L'évolution très rapide de l'économie, la globalisation des marchés et l'incertitude liée aux conditions économiques obligent les organisations, autant les petites que les grandes, à faire un effort systématique pour connaître à tout moment leur situation actuelle, pour prévoir où elles seront dans quelques mois ou quelques années et pour analyser les stratégies et les opportunités en accord avec les buts et les objectifs qu’elles se sont donnés. Les entreprises se sont dotées au cours des vingt dernières années, de systèmes informatisés de plus en plus complexes afin de connaître leurs résultats financiers. Mais ces systèmes se sont graduellement alourdis au cours des ans, si bien qu'ils ne peuvent montrer de façon rapide la véritable situation de la firme. Pourtant, l’administrateur a besoin de cette information de façon instantanée. De plus, les systèmes informatisés implantés dans les entreprises n'ont pas été développés pour simuler l'avenir : le gestionnaire est souvent obligé de se fier à son instinct. Cependant, à cause de la vitesse vertigineuse à laquelle elle évolue, de la multitude de problèmes différents et complexes qui l’assaillent et de la concurrence de plus en plus difficile et féroce, l'entreprise qui n'a pas à sa disposition des outils informatiques efficaces risque de se faire dépasser par ses concurrentes. Heureusement, les derniers développements technologiques en micro et en mini-informatique permettent aux organisations de résoudre plus facilement beaucoup de leurs problèmes. L'avènement récent de logiciels spécialisés dans la livraison aux décideurs des informations essentielles à la bonne gestion et à la prise de décision permet à l'entreprise de demeurer très compétitive. Ces systèmes sont très faciles à opérer: le dirigeant a accès à l’information sans assistance technique. Ces nouveaux outils permettent au cadre de s'assurer que son organisation est en bonne santé ou, le cas échéant, de corriger les problèmes. Ces systèmes, communément appelés des tableaux de bord pour administrateurs, aident ceux-ci à analyser les tendances et à chiffrer les différentes stratégies. La présente étude vise à appliquer aux cégeps ce type de système informatique.

A tableau system for Quasi-hybrid logic

Hybrid logic is a valuable tool for specifying relational structures, at the same time that allows defining accessibility relations between states, it provides a way to nominate and make mention to what happens at each specific state. However, due to the many sources nowadays available, we may need to deal with contradictory information. This is the reason why we came with the idea of Quasi-hybrid logic, which is a paraconsistent version of hybrid logic capable of dealing with inconsistencies in the information, written as hybrid formulas. In [5] we have already developed a semantics for this paraconsistent logic. In this paper we go a step forward, namely we study its proof-theoretical aspects. We present a complete tableau system for Quasi-hybrid logic, by combining both tableaux for Quasi-classical and Hybrid logics.

Tableau de Bord: uma ferramenta competitiva

Em pleno século XXI, onde a globalização é uma realidade, tenho constatado na minha atividade profissional, que uma grande parte das empresas portuguesas ainda não conseguiu interiorizar este fato, ou seja, ainda não perceberam que os seus stakeholders, especialmente clientes, fornecedores e concorrentes, estão em qualquer parte do globo e não ao virar da esquina. Assim, para fazer face a esta realidade do “viver global” é fundamental responder através do “pensar glocal”. Este “pensar glocal”, significa perceber que o paradigma dos negócios se alterou por completo e que, presentemente o segredo não é a alma do negócio, a alma que colocamos no negócio, essa sim é que é o segredo. O sucesso da gestão e a consequente longevidade das organizações não é compatível com filosofias como “navegar à vista” ou “gestão na base de caixa”. É fundamental gerir com base em horizontes de curto, médio e longo prazo, definindo estratégias e objetivos, apoiadas nas vantagens competitivas e nos fatores críticos de sucesso que cada organização possui. Para que seja possível alcançar esta proeza, é impreterível gerir com método, observação, análise, rigor, rapidez e perspicácia, e apoiando-se sempre em ferramentas de gestão para que tudo esteja devidamente planificado e estruturado e todos os membros da organização se encontrem enquadrados e em sintonia com os objetivos da organização. Face a toda esta realidade, o presente trabalho pretende contribuir para uma melhor compreensão do controlo de gestão, através da utilização de uma poderosa ferramenta como é o Tableaux de Bord, mostrando a forma como pode ser aplicado em micro, pequenas e médias empresas, dotando-as de uma forte vantagem competitiva.

Numerical methods for second-order stochastic differential equations

We seek numerical methods for second‐order stochastic differential equations that reproduce the stationary density accurately for all values of damping. A complete analysis is possible for scalar linear second‐order equations (damped harmonic oscillators with additive noise), where the statistics are Gaussian and can be calculated exactly in the continuous‐time and discrete‐time cases. A matrix equation is given for the stationary variances and correlation for methods using one Gaussian random variable per timestep. The only Runge–Kutta method with a nonsingular tableau matrix that gives the exact steady state density for all values of damping is the implicit midpoint rule. Numerical experiments, comparing the implicit midpoint rule with Heun and leapfrog methods on nonlinear equations with additive or multiplicative noise, produce behavior similar to the linear case.

Trashtopia by Maison Briz Vegas

Description of the Work Trashtopia was a fashion exhibition at Craft Queensland’s Artisan gallery showcasing outfits made entirely from rubbish materials. The exhibition was part of an on-going series by the Queensland Fashion Archives, called Remember or Revive. Maison Briz Vegas designers, Carla Binotto and Carla van Lunn created a dystopian beach holiday tableau referencing mid-century Californian and Gold Coast beach culture and style, and today’s plastic pollution of the world’s oceans. The display engaged a popular audience with ideas about environmental destruction and climate change while bringing twentieth and twenty-first century consumer and leisure culture into question. The medium of fashion was used as a means of amusement and provocation. The fashion objects and installation questioned current mores about the material value of rubbish and the installation was also a work of environmental activism. Statement of the Research Component The work was framed by critical reflections of contemporary consumer culture and research fields questioning value in waste materials and fashion objects. The work is situated in the context of conceptual and experimental fashion design practice and fashion presentation. The exhibited work transgressed the conventional production methods and material choice of designer fashion garments, for example, discarded plastic shopping bags were painstakingly shredded to mimic ostrich feathers. The viewer was prompted to reflect on the materiality of rubbish and its potential for transformation. The exhibition also sits in the context of culture jamming and contemporary activist practice. The work references and subverts twentieth century beach holiday culture, contrasting resort wear with a contemporary picture of plastic pollution of the oceans and climate change. Hawaiian style prints contained a playful and dark narrative of dying marine-life and the viewer was invited to take a “Greetings from Trashtopia” postcard depicting fashion models floating in oceans of plastic rubbish. This reflective creative practice sought to address the question of whether fashion made from recycled rubbish materials can critically and emotionally engage viewers with questions about contemporary consumer culture and material value. This work presents an innovative model of fashion design practice in which rubbish materials are transformed into designer garments and rubbish is placed centre stage in the public presentation of the designs. In overturning the traditional model of fashion presentation, the viewer is also given a deeper connection to the recycling process and complex ideas of waste and value. In 2015 two outfits from the exhibition were selected, along with works from three leading Australian fashion labels, and four leading New Zealand labels, for a commemorative ANZAC fashion collection shown at iD Dunedin Fashion Week. The show titled, “Together Alone, revisited” reprised an Australian and New Zealand fashion exhibition first held at the National Gallery of Victoria in 2009.

A computational algorithm for the verification of tautologies in propositional calculus

A computational algorithm (based on Smullyan's analytic tableau method) that varifies whether a given well-formed formula in propositional calculus is a tautology or not has been implemented on a DEC system 10. The stepwise refinement approch of program development used for this implementation forms the subject matter of this paper. The top-down design has resulted in a modular and reliable program package. This computational algoritlhm compares favourably with the algorithm based on the well-known resolution principle used in theorem provers.

Animal Spirits

Animal Spirits is multi-channel video portrait of key personalities involved in the Global Financial Crisis. The four-screen installation displays these twelve decapitated apostles of free-market economic theory in a tableau of droning pontification. Trapped in a purgatorial loop, they endlessly spout vague and obfuscating explanations and defenses of their ideologies and (in)actions. The work takes a creatively quotidian approach to understanding the language of economics and the financial services industry. Through its endless loop of sound, image, and spoken text, the installation examines some of the ideas, narratives and power dynamics that foster and reward hubris and greed.

Automatic verification of distributed logic specifications

Formal specification is vital to the development of distributed real-time systems as these systems are inherently complex and safety-critical. It is widely acknowledged that formal specification and automatic analysis of specifications can significantly increase system reliability. Although a number of specification techniques for real-time systems have been reported in the literature, most of these formalisms do not adequately address to the constraints that the aspects of 'distribution' and 'real-time' impose on specifications. Further, an automatic verification tool is necessary to reduce human errors in the reasoning process. In this regard, this paper is an attempt towards the development of a novel executable specification language for distributed real-time systems. First, we give a precise characterization of the syntax and semantics of DL. Subsequently, we discuss the problems of model checking, automatic verification of satisfiability of DL specifications, and testing conformance of event traces with DL specifications. Effective solutions to these problems are presented as extensions to the classical first-order tableau algorithm. The use of the proposed framework is illustrated by specifying a sample problem.

Invariant-free deduction systems for temporal logic

In this thesis we propose a new approach to deduction methods for temporal logic. Our proposal is based on an inductive definition of eventualities that is different from the usual one. On the basis of this non-customary inductive definition for eventualities, we first provide dual systems of tableaux and sequents for Propositional Linear-time Temporal Logic (PLTL). Then, we adapt the deductive approach introduced by means of these dual tableau and sequent systems to the resolution framework and we present a clausal temporal resolution method for PLTL. Finally, we make use of this new clausal temporal resolution method for establishing logical foundations for declarative temporal logic programming languages. The key element in the deduction systems for temporal logic is to deal with eventualities and hidden invariants that may prevent the fulfillment of eventualities. Different ways of addressing this issue can be found in the works on deduction systems for temporal logic. Traditional tableau systems for temporal logic generate an auxiliary graph in a first pass.Then, in a second pass, unsatisfiable nodes are pruned. In particular, the second pass must check whether the eventualities are fulfilled. The one-pass tableau calculus introduced by S. Schwendimann requires an additional handling of information in order to detect cyclic branches that contain unfulfilled eventualities. Regarding traditional sequent calculi for temporal logic, the issue of eventualities and hidden invariants is tackled by making use of a kind of inference rules (mainly, invariant-based rules or infinitary rules) that complicates their automation. A remarkable consequence of using either a two-pass approach based on auxiliary graphs or aone-pass approach that requires an additional handling of information in the tableau framework, and either invariant-based rules or infinitary rules in the sequent framework, is that temporal logic fails to carry out the classical correspondence between tableaux and sequents. In this thesis, we first provide a one-pass tableau method TTM that instead of a graph obtains a cyclic tree to decide whether a set of PLTL-formulas is satisfiable. In TTM tableaux are classical-like. For unsatisfiable sets of formulas, TTM produces tableaux whose leaves contain a formula and its negation. In the case of satisfiable sets of formulas, TTM builds tableaux where each fully expanded open branch characterizes a collection of models for the set of formulas in the root. The tableau method TTM is complete and yields a decision procedure for PLTL. This tableau method is directly associated to a one-sided sequent calculus called TTC. Since TTM is free from all the structural rules that hinder the mechanization of deduction, e.g. weakening and contraction, then the resulting sequent calculus TTC is also free from this kind of structural rules. In particular, TTC is free of any kind of cut, including invariant-based cut. From the deduction system TTC, we obtain a two-sided sequent calculus GTC that preserves all these good freeness properties and is finitary, sound and complete for PLTL. Therefore, we show that the classical correspondence between tableaux and sequent calculi can be extended to temporal logic. The most fruitful approach in the literature on resolution methods for temporal logic, which was started with the seminal paper of M. Fisher, deals with PLTL and requires to generate invariants for performing resolution on eventualities. In this thesis, we present a new approach to resolution for PLTL. The main novelty of our approach is that we do not generate invariants for performing resolution on eventualities. Our method is based on the dual methods of tableaux and sequents for PLTL mentioned above. Our resolution method involves translation into a clausal normal form that is a direct extension of classical CNF. We first show that any PLTL-formula can be transformed into this clausal normal form. Then, we present our temporal resolution method, called TRS-resolution, that extends classical propositional resolution. Finally, we prove that TRS-resolution is sound and complete. In fact, it finishes for any input formula deciding its satisfiability, hence it gives rise to a new decision procedure for PLTL. In the field of temporal logic programming, the declarative proposals that provide a completeness result do not allow eventualities, whereas the proposals that follow the imperative future approach either restrict the use of eventualities or deal with them by calculating an upper bound based on the small model property for PLTL. In the latter, when the length of a derivation reaches the upper bound, the derivation is given up and backtracking is used to try another possible derivation. In this thesis we present a declarative propositional temporal logic programming language, called TeDiLog, that is a combination of the temporal and disjunctive paradigms in Logic Programming. We establish the logical foundations of our proposal by formally defining operational and logical semantics for TeDiLog and by proving their equivalence. Since TeDiLog is, syntactically, a sublanguage of PLTL, the logical semantics of TeDiLog is supported by PLTL logical consequence. The operational semantics of TeDiLog is based on TRS-resolution. TeDiLog allows both eventualities and always-formulas to occur in clause heads and also in clause bodies. To the best of our knowledge, TeDiLog is the first declarative temporal logic programming language that achieves this high degree of expressiveness. Since the tableau method presented in this thesis is able to detect that the fulfillment of an eventuality is prevented by a hidden invariant without checking for it by means of an extra process, since our finitary sequent calculi do not include invariant-based rules and since our resolution method dispenses with invariant generation, we say that our deduction methods are invariant-free.

共代数中的互模拟证明方法及其应用

本论文主要研究共代数中的互模拟证明方法及其应用两个方面。 代数理论已被证实在计算机科学中具有广泛的应用，其对偶概念——共代数理论是近年来兴起的一个理论，它在描述无穷状态系统方面具有明显的优势。 因此，我们在本文中以共代数作为抽象的研究模型。 因为互模拟判定中的up-to方法能够非常有效地加速判定过程，我们首先将该方法从传统的集合论中 扩展到共代数理论。作为Sangiorgi的可靠函数的扩展，我们引入了一致函数。因此， 为了证明某个二元关系中的进程对都是互模拟等价的，只要证明该关系前进到其在某个一致函数作用下得到的新关系中即可。 另外，我们给出了span-互模拟和ref-互模拟之间的等价转换关系，并且，利用该结果证明了共代数中原有的up-to方法 都能被一致函数所覆盖。 一致函数是为单个函子$F$定义的。但是，当$F$是某种类型的多项式函子时，有可能存在一些 函数，它们与$F$的某些子函子一致却不与整个$F$一致。因此，我们将一致函数进一步扩展，定义 联合一致函数，它是那些只与某些子函子一致的函数在一定条件下的组合。联合一致函数使用起来和一致函数一样，能够用来产生 新的up-to证明方法。另外，我们也相应地给出了传统并发理论中的联合一致函数概念，并且利用它给出了 弱互模拟的up-to方法。 在抽象的共代数模型中给出一般化的up-to方法之后，本文继续研究其在具体的无穷状态系统，即 BPA系统上的应用。Caucal的self-互模拟理论在 BPA系统的互模拟判定算法中起着关键作用，而它恰恰 是运用up-to方法协助互模拟判定的一个典范。 因为一个BPA系统也是一个共代数，我们在共代数理论中利用一致函数证明了该理论。 同时，本文给出了一个tableau算法，用来判定包含normed 与unnormed BPA进程的全BPA系统的互模拟等价问题。该算法非常直接且易于理解。 利用该tableau算法，我们证明了Hans H\"{u}ttel 和 Colin Stirling 为normed BPA进程设计的等式理论对于全BPA系统同样是可靠的与完备的。

构建度量区间时序逻辑的时间自动机

实时系统的安全性至关重要，使用模型检测工具对其进行形式化分析是提高 其安全性的重要手段。我们已有的实时系统模型检测工具CTAV 目前可以验证 LTL 描述的性质。本文工作的最终目的是让CTAV 能够验证实时时序逻辑，即， 使得CTAV 同样可以直接验证由实时时序逻辑描述的连续时间域上的实时性质。 度量区间时序逻辑MITL 是常用的一种关于实时系统的性质规范语言。已有 不少文献讨论过MITL 到时间Büchi 自动机的转换，但由于过程较复杂，大多数 仅限于理论研究，并没有与时间Büchi 自动机的空性判定过程结合成为一个可用 的关于MITL 的模型检测工具。 为了开发可用的关于MITL 性质的模型检测工具，本文采用与CTAV 中待验 证系统模型一致的pointwise 语义模型，选取了MITL 的一个可以较高效的进行模型检测的子类——MITL≤/<。在表达能力方面，这个子集能够描述实时系统模 型检测实际过程中常见的实时性质。 本文给出了将MITL≤/<公式转化为等价的基于迁移的扩展时间Büchi 自动机 的算法过程，并讨论了转化中逻辑公式重写规则的正确性和完备性问题。基于迁 移的扩展时间Büchi 自动机是时间Büchi 自动机的一种变体。二者最主要的区别在于它们采用了不同类型的Büchi 接受条件。文中给出的构造算法是将原先应用于非实时领域的Tableau 方法扩展调整，并应用于实时连续领域。Tableau 方法的关键之一是公式重写规则。而为了保证结果自动机仅存在有限多个状态，在重写规则中定义不动子公式是至关重要的。本文给出的在pointwise 语义模型下的公式重写规则，借用了此前在continuous 语义模型下已有的将时钟变量作为时序算子的约束直接引入公式中来保证重写规则中存在不动子公式的思想，并对其进行了修改，使原先性质自动机的时钟递减变为时钟递增，与系统自动机中的时钟行走方式一致。这省去了下一步将性质自动机和系统自动机相乘判空时，因为时钟行走方式不一致而引起的麻烦。另外，本文将MITL≤/<中的某些公式扩展为包含时钟约束的新的公式。这样，在定义重写公式时，不仅保证重写规则中存在不动子公式，也保证结果自动的前进性。 本文还根据构造算法实现了转化工具MITLCon。与Marc Geilen 和Dennis Dames 实现的逻辑转化工具相比，MITLCon 显著地减少了结果自动机节点和迁 移的数量，从而降低了结果自动机的大小，有利于进一步的模型检测过程。