Arbetets syfte är att undersöka hur högstadieelever för matematiskt resonemang. De frågeställningar som studien inriktas på är vilka lösningsstrategier elever väljer då de resonerar matematiskt såväl som vad  det finns för skillnader och likheter mellan de yngre elevernas lösningar och de äldre elevernas lösningar. Undersökningen genomfördes i två klasser, den ena i årskurs 8 och den andra i årskurs 9, på en grundskola. Eleverna fick lösa uppgifter, vilka uppmanade dem att föra matematiskt resonemang, individuellt. Resultatet av studien visar att majoriteten av undersökta elever har valt att resonera deduktivt. Jämförelsen av elevers lösningar i två årskurser visar att årskurs 9 elevers resonemangsföring präglas av större förtrogenhet med den algebraiska demonstrationen. Resultatet visar även att elever med högre kunskaper om algebra oftare visar benägenheter till att vidaregeneralisera de givna påståendena. / The purpose of this study is to examine secondary school students’ strategies of reasoning. The study inquires into which strategies students choose when reasoning mathematically as well as differences and similarities between the younger students’ solutions and the older students’ solutions. The study was conducted in two classes, in years 8 and 9 respectively, at a secondary school. The students were asked to solve tasks, which encouraged them to reason mathematically, on individual basis. The study revealed that the majority of students had chosen to reason deductively. The comparison of students’ presented answers in two years showed that the ninth-graders’ solutions are characterized of greater skill when it comes to algebraic demonstrations. The results of the study also reveal that students with stronger algebraic abilities attempt more often to generalize the given mathematical statements further.

Om man ser på de bästa nu kända algoritmerna för att avgöra satisfierbarhet hos logiska formler så är de allra flesta baserade på den så kallade DPLL-metoden utökad med klausulinlärning. De två viktigaste gränssättande faktorerna för sådana algoritmer är hur mycket tid och minne de använder, och att förstå sig på detta är därför en fråga som har stor praktisk betydelse. Inom området beviskomplexitet svarar tids- och minnesåtgång mot längd och minne hos resolutionsbevis för formler i konjunktiv normalform (CNF-formler). En lång rad arbeten har studerat dessa mått och även jämfört dem med bredden av bevis, ett annat mått som visat sig höra nära samman med både längd och minne. Mer formellt är längden hos ett bevis antalet rader, dvs. klausuler, bredden är storleken av den största klausulen, och minnet är maximala antalet klausuler som man behöver komma ihåg samtidigt om man under bevisets gång bara får dra nya slutsatser från klausuler som finns sparade. För längd och bredd har man lyckats visa en rad starka resultat men förståelsen av måttet minne har lämnat mycket i övrigt att önska. Till exempel så är det känt att minnet som behövs för att bevisa en formel är minst lika stort som den nödvändiga bredden, men det har varit en öppen fråga om minne och bredd kan separeras eller om de två måtten mäter "samma sak" i den meningen att de alltid är asymptotiskt lika stora för en formel. Det har också varit okänt om det faktum att det finns ett kort bevis för en formel medför att formeln också kan bevisas i litet minne (motsvarande påstående är sant för längd jämfört med bredd) eller om det tvärtom kan vara så att längd och minne är "helt orelaterade" på så sätt att även korta bevis kan kräva maximal mängd minne. I denna avhandling presenterar vi först ett förenklat bevis av trade-off-resultatet för längd jämfört med minne i (Hertel och Pitassi 2007) och visar hur samma idéer kan användas för att visa ett par andra exponentiella avvägningar i relationerna mellan olika beviskomplexitetsmått för resolution. Sedan visar vi att det finns formler som kan bevisas i linjär längd och konstant bredd men som kräver en mängd minne som växer logaritmiskt i formelstorleken, vilket vi senare förbättrar till kvadratroten av formelstorleken. Dessa resultat separerar således minne och bredd. Genom att använda andra men besläktade idéer besvarar vi därefter frågan om hur minne och längd förhåller sig till varandra genom att separera dem på starkast möjliga sätt. Mer precist visar vi att det finns CNF-formler av storlek O(n) som har resolutionbevis i längd O(n) och bredd O(1) men som kräver minne minst Omega(n/log n). Det gemensamma temat för dessa resultat är att vi studerar formler som beskriver stenläggningsspel, eller pebblingspel, på riktade acykliska grafer. Vi bevisar undre gränser för det minne som behövs för den så kallade pebblingformeln över en graf uttryckt i det svart-vita pebblingpriset för grafen i fråga. Slutligen observerar vi att vår optimala separation av minne och längd i själva verket är ett specialfall av en mer generell sats. Låt F vara en CNF-formel och f:{0,1}^d->{0,1} en boolesk funktion. Ersätt varje variabel x i F med f(x_1, ..., x_d) och skriv om denna nya formel på naturligt sätt som en CNF-formel F[f]. Då gäller, givet att F och f har rätt egenskaper, att F[f] kan bevisas i resolution i väsentligen samma längd och bredd som F, men att den minimala mängd minne som behövs för F[f] är åtminstone lika stor som det minimala antalet variabler som måste förekomma samtidigt i ett bevis för F. / Most state-of-the-art satisfiability algorithms today are variants of the DPLL procedure augmented with clause learning. The two main bottlenecks for such algorithms are the amounts of time and memory used. Thus, understanding time and memory requirements for clause learning algorithms, and how these requirements are related to one another, is a question of considerable practical importance. In the field of proof complexity, these resources correspond to the length and space of resolution proofs for formulas in conjunctive normal form (CNF). There has been a long line of research investigating these proof complexity measures and relating them to the width of proofs, another measure which has turned out to be intimately connected with both length and space. Formally, the length of a resolution proof is the number of lines, i.e., clauses, the width of a proof is the maximal size of any clause in it, and the space is the maximal number of clauses kept in memory simultaneously if the proof is only allowed to infer new clauses from clauses currently in memory. While strong results have been established for length and width, our understanding of space has been quite poor. For instance, the space required to prove a formula is known to be at least as large as the needed width, but it has remained open whether space can be separated from width or whether the two measures coincide asymptotically. It has also been unknown whether the fact that a formula is provable in short length implies that it is also provable in small space (which is the case for length versus width), or whether on the contrary these measures are "completely unrelated" in the sense that short proofs can be maximally complex with respect to space. In this thesis, as an easy first observation we present a simplified proof of the recent length-space trade-off result for resolution in (Hertel and Pitassi 2007) and show how our ideas can be used to prove a couple of other exponential trade-offs in resolution. Next, we prove that there are families of CNF formulas that can be proven in linear length and constant width but require space growing logarithmically in the formula size, later improving this exponentially to the square root of the size. These results thus separate space and width. Using a related but different approach, we then resolve the question about the relation between space and length by proving an optimal separation between them. More precisely, we show that there are families of CNF formulas of size O(n) that have resolution proofs of length O(n) and width O(1) but for which any proof requires space Omega(n/log n). All of these results are achieved by studying so-called pebbling formulas defined in terms of pebble games over directed acyclic graphs (DAGs) and proving lower bounds on the space requirements for such formulas in terms of the black-white pebbling price of the underlying DAGs. Finally, we observe that our optimal separation of space and length is in fact a special case of a more general phenomenon. Namely, for any CNF formula F and any Boolean function f:{0,1}^d->{0,1}, replace every variable x in F by f(x_1, ..., x_d) and rewrite this new formula in CNF in the natural way, denoting the resulting formula F[f]. Then if F and f have the right properties, F[f] can be proven in resolution in essentially the same length and width as F but the minimal space needed for F[f] is lower-bounded by the number of variables that have to be mentioned simultaneously in any proof for F. / QC 20100831

We present a series of improvements to the Hybrid system, a formal theory implemented in Isabelle/HOL to support specifying and reasoning about formal systems using higher-order abstract syntax (HOAS). We modify Hybrid's type of terms, which is built definitionally in terms of de Bruijn indices, to exclude at the type level terms with `dangling' indices. We strengthen the injectivity property for Hybrid's variable-binding operator, and develop rules for compositional proof of its side condition, avoiding conversion from HOAS to de Bruijn indices. We prove representational adequacy of Hybrid (with these improvements) for a lambda-calculus-like subset of Isabelle/HOL syntax, at the level of set-theoretic semantics and without unfolding Hybrid's definition in terms of de Bruijn indices. In further work, we prove an induction principle that maintains some of the benefits of HOAS even for open terms. We also present a case study of the formalization in Hybrid of a small programming language, Mini-ML with mutable references, including its operational semantics and a type-safety property. This is the largest case study in Hybrid to date, and the first to formalize a language with mutable references. We compare four variants of this formalization based on the two-level approach adopted by Felty and Momigliano in other recent work on Hybrid, with various specification logics (SLs), including substructural logics, formalized in Isabelle/HOL and used in turn to encode judgments of the object language. We also compare these with a variant that does not use an intermediate SL layer. In the course of the case study, we explore and develop new proof techniques, particularly in connection with context invariants and induction on SL statements.

We present a series of improvements to the Hybrid system, a formal theory implemented in Isabelle/HOL to support specifying and reasoning about formal systems using higher-order abstract syntax (HOAS). We modify Hybrid's type of terms, which is built definitionally in terms of de Bruijn indices, to exclude at the type level terms with `dangling' indices. We strengthen the injectivity property for Hybrid's variable-binding operator, and develop rules for compositional proof of its side condition, avoiding conversion from HOAS to de Bruijn indices. We prove representational adequacy of Hybrid (with these improvements) for a lambda-calculus-like subset of Isabelle/HOL syntax, at the level of set-theoretic semantics and without unfolding Hybrid's definition in terms of de Bruijn indices. In further work, we prove an induction principle that maintains some of the benefits of HOAS even for open terms. We also present a case study of the formalization in Hybrid of a small programming language, Mini-ML with mutable references, including its operational semantics and a type-safety property. This is the largest case study in Hybrid to date, and the first to formalize a language with mutable references. We compare four variants of this formalization based on the two-level approach adopted by Felty and Momigliano in other recent work on Hybrid, with various specification logics (SLs), including substructural logics, formalized in Isabelle/HOL and used in turn to encode judgments of the object language. We also compare these with a variant that does not use an intermediate SL layer. In the course of the case study, we explore and develop new proof techniques, particularly in connection with context invariants and induction on SL statements.

In this thesis we see deductive systems for classical propositional and predicate logic which use deep inference, i.e. inference rules apply arbitrarily deep inside formulas, and a certain symmetry, which provides an involution on derivations. Like sequent systems, they have a cut rule which is admissible. Unlike sequent systems, they enjoy various new interesting properties. Not only the identity axiom, but also cut, weakening and even contraction are reducible to atomic form. This leads to inference rules that are local, meaning that the effort of applying them is bounded, and finitary, meaning that, given a conclusion, there is only a finite number of premises to choose from. The systems also enjoy new normal forms for derivations and, in the propositional case, a cut elimination procedure that is drastically simpler than the ones for sequent systems.

Olika aktörer på fastighetsmarknaden har svårigheter att värdesätta kommersiella fastigheter på grund av den minskade transparensen på marknaden. Den minskade transparensen är ett resultat av att färre fastigheter överlåts genom köpehandling idag. Syftet med denna studie är att skapa en ökad förståelse på fastighetsmarknaden och på så vis underlätta för olika aktörer på fastighetsmarknaden att genomföra marknadsanalyser. Målet är att utreda varför vissa bolag väljer att överlåta sina fastigheter med köpehandling istället för att överlåta fastigheter genom att paketera den i ett dotterbolag. Två rättsfall har studerats för att få rättsväsendets bedömningar. Genom rättsfallen kunde det konstateras att det råder en viss osäkerhet i hur beskattningen ska genomföras vid fastighetsöverlåtelser. Denna osäkerhet kan leda till att bolagen väljer att överlåta fastigheterna genom köpehandling där rättsläget är mycket tydligare.   För att utreda varför bolag väljer att överlåta kommersiella fastigheter genom köpehandling har en intervjustudie genomförts. Intervjustudien påvisade att bolagens val av överlåtelseform är beroende av de för- och nackdelar samt de skattemässiga konsekvenser som överlåtelsen medför. Intervjustudien visar även att enklare överlåtelseprocesser föredras av bolagen samt att de säljande bolagen vill uppnå en ekonomisk vinning genom överlåtelserna av fastigheterna.   Slutsatsen är att säljarens val av överlåtelseform är beroende på utfallet av kalkyleringsmetoden, köparens påverkan på överlåtelseformen samt hur komplicerad överlåtelseprocessen får vara. Den ökade transparensen som överlåtelser genom köpehandling bidrar till gör att de olika aktörernas marknadsanalyser på fastighetsmarknaden kan förenklas och bli mer tillförlitliga. Utöver detta avser regeringen att tillsätta en utredning angående skatteplanering i samband med då fastigheter paketeras i bolag. Beroende på vad regeringens utredning får för utfall kan antalet överlåtelser på fastighetsmarknaden ändras vilket skulle kunna vara intressant att undersöka i en framtida studie. / Different participants in the real estate market have difficulty in valuing commercial real estate due to reduced market transparency. The reduced transparency is a result of fewer properties being transferred by way of document of purchase today. The purpose of this study is to create a better understanding of the property market and be able to provide market participant with an improved understanding how to analyze this market. The objective is to investigate why some companies choose to sell properties by way of document of purchase instead of transferring the property by using a limited company structure. Two legal cases have been reviewed for judicial assessments. The court cases analysis showed the degree of turnover of property transfers can lead to uncertainty in terms of possible tax implications. This uncertainty might lead to companies choosing to transfer properties by way of document of purchase due to the much clearer legal position.   An interview study has been conducted to investigate why companies transfer commercial properties through the use of purchase document. The study showed that companies’ choice of transfer form is dependent on the advantages and disadvantages of the form together with possible tax implications. The interview study also showed a simple transfer process is preferred together with financial gains when selling properties.   The conclusion is that the seller’s preferred choice of transfer form is dependent on the outcome of the project models, the purchasers’ impact and how complicated the transfer process may be. The increased level of transparency achieved by using document of purchase makes it easier for participants in the real estate market to conduct market analysis and also to make the results more reliable. In addition to this the Swedish government intends to launch an investigation into potential effects of tax planning in connection with the use of limited corporate structures. The number of transferals in the property market could potentially change dependent on the outcome of the government’s investigation and if so this could be an interesting topic for a future study.

published_or_final_version / Education / Master / Master of Education

Le raisonnement assisté par ordinateur joue un rôle crucial en informatique et en logique mathématique, de la programmation logique à la déduction automatique, en passant par les assistants à la démonstration. Le but de cette thèse est la conception d'un cadre général où différentes techniques de raisonnement assisté par ordinateur peuvent être implémentées, pour que ces dernières puissent collaborer, être généralisées, et être implémentées de manière plus sûre. Le cadre que je propose est un calcul des séquents appelé LKp(T), qui généralise un système de la littérature à la présence d'une théorie pour laquelle nous avons une procédure de décision, comme l'arithmétique linéaire. Cette thèse développe la méta-théorie de LKp(T), avec par exemple la propriété de complétude logique. Nous montrons ensuite comment le système spécifie une procédure de recherche de preuve qui émule une technique connue du domaine de la Satisfiabilité-modulo-théories appelée DPLL(T). Enfin, les tableaux de clauses et les tableaux de connexions sont d'autres techniques populaires en déduction automatique, d'une nature relativement différente de DPLL. Cette thèse décrit donc également comment ces techniques de tableaux peuvent être décrites en termes de recherche de preuve dans LKp(T). La simulation est donnée à la fois pour la logique propositionnelle et la logique du premier ordre, ce qui ouvre de nouvelles perspectives de généralisation et de collaboration entre les techniques de tableaux et DPLL, même en présence d'une théorie.

Les technologies de l’information entraînent de profondes transformations dans nos façons d’apprendre et de socialiser ; de lire et d’écrire. Ces changements ne sont pas sans conséquence sur de nombreuses institutions, juridiques ou non. Créées au fil du temps et adaptées à une réalité qu’elles avaient internalisée, elles doivent aujourd’hui comprendre et s’adapter au changement. L’écrit est une de ces institutions. Sa place dans le droit civil est le fruit de centaines d’années de cohabitation et le droit y a vu un allié stable. Mais autrefois facilitateur, l’écrit devient obstacle alors que les technologies de l’information, affranchies du papier, sont utilisées dans des situations juridiques. Comment adapter la notion d’écrit – et celles de l’original et de la signature – alors qu’il n’est question que de données abstraites sous forme numérique ? C’est là l’objet de ce mémoire. Suite à une étude de la notion d’écrit dans le temps, de son affirmation à son bouleversement, nous étudierons les outils juridiques (traditionnels ou récents, comme les principes de neutralité technologique et d’équivalence fonctionnelle) à la disposition du droit civil pour constamment s’adapter à des situations changeantes. Enfin, dans une perspective plus pratique, nous verrons le traitement qu’ont fait divers législateurs, de l’écrit électronique. Nous terminerons par une analyse plus précise des dispositions québécoises relatives à l’écrit électronique. Les principes étudiés dans ce mémoire sont susceptibles de s’appliquer à d’autres situations similaires. / Information technology has completely modified our way of learning, socialising, reading and writing. These changes have also affected numerous institutions. Developed over many years and adapted to a reality they internalised, they now have to understand the nature of the changes taking place and adapt to them. The legal concept of “writing” is such an institution. Its place in the realm of civil law is the result of hundreds of years of cohabitation. The legal system has found a great ally in “writings”. However, although “writing” has been seen as an enabler in the past, the use of information technologies in legal circumstances has turned it into an obstacle. How are we going to adapt the notion of writing – and those of original and signature – when talking about digital data ? This is the topic of our thesis. Following a historical study of the concept of “writing”, from its inception to its current state of crisis, we will analyse the legal tools made available to civil law (whether they be traditional or recent, such as the technological neutrality, and functional equivalence principles) in order to adapt to a constantly changing technological landscape. On a more practical level, we will study how different legislators have addressed electronic documents. Our study will conclude with an analysis of Quebec legislation pertaining to electronic documents. The principles studied in this thesis should be applicable to other similar situations.

L’un des buts de l’apprentissage des mathématiques est le développement du raisonnement et celui-ci participe à la compréhension des mathématiques. Très liée au raisonnement, la notion de preuve est aussi fondamentale à l’apprentissage des mathématiques, car elle permet d’établir la validité d’arguments mathématiques et de conférer un sens à différents concepts à travers l’explication de l’organisation logique du travail effectué. Toutefois, malgré l’importance accordée au développement de différents types de raisonnements, plusieurs élèves éprouvent des difficultés lorsqu’ils sont appelés à concevoir ou à évaluer des preuves. Dans le cadre de cette recherche, nous avons étudié l’impact de l’utilisation d’un forum électronique sur le développement d’habiletés de validation algébrique ainsi que sur le développement d’habiletés en lien avec l’évaluation de preuves en algèbre chez des élèves de 13 et 14 ans du Nouveau-Brunswick et du Québec. Les résultats laissent supposer que l’utilisation du forum électronique encourage le passage des preuves pragmatiques aux preuves intellectuelles, en plus de favoriser une utilisation adéquate des règles du débat mathématique. / One of the goals of learning mathematics is the development of reasoning, because it is essential to understand mathematics. Closely related to reasoning, the notion of proof is also fundamental in the learning of mathematics, because it allows students to establish the validity of mathematical arguments and put a sense on various concepts through logical explanation of their work. However, in spite of the importance placed on the development of the capacity to reason mathematically, several students are confronted with difficulties during the development or the evaluation of proofs. This study examined the impact of the use of a discussion forum on the development of algebraic validation skills as well as on the development of skills linked with the evaluation of the proof process in algebra with 13 and 14 year old students from New Brunswick and Quebec (Canada). The results lead us to believe that the use of the electronic forum encourages the passage from pragmatic proofs to intellectual proofs. It also seems to facilitate an adequate use of the rules of the mathematical debate.