Change search
Refine search result
12 1 - 50 of 88
CiteExportLink to result list
Permanent link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Rows per page
  • 5
  • 10
  • 20
  • 50
  • 100
  • 250
Sort
  • Standard (Relevance)
  • Author A-Ö
  • Author Ö-A
  • Title A-Ö
  • Title Ö-A
  • Publication type A-Ö
  • Publication type Ö-A
  • Issued (Oldest first)
  • Issued (Newest first)
  • Created (Oldest first)
  • Created (Newest first)
  • Last updated (Oldest first)
  • Last updated (Newest first)
  • Disputation date (earliest first)
  • Disputation date (latest first)
  • Standard (Relevance)
  • Author A-Ö
  • Author Ö-A
  • Title A-Ö
  • Title Ö-A
  • Publication type A-Ö
  • Publication type Ö-A
  • Issued (Oldest first)
  • Issued (Newest first)
  • Created (Oldest first)
  • Created (Newest first)
  • Last updated (Oldest first)
  • Last updated (Newest first)
  • Disputation date (earliest first)
  • Disputation date (latest first)
Select
The maximal number of hits you can export is 250. When you want to export more records please use the Create feeds function.
  • 1. Aceto, Luca
    et al.
    Della Monica, Dario
    Goranko, Valentin
    Stockholm University, Faculty of Humanities, Department of Philosophy. University of Johannesburg, South Africa.
    Ingólfsdóttir, Anna
    Montanari, Angelo
    Sciavicco, Guido
    A complete classification of the expressiveness of interval logics of Allen’s relations: the general and the dense cases2016In: Acta Informatica, ISSN 0001-5903, E-ISSN 1432-0525, Vol. 53, no 3, p. 207-246Article in journal (Refereed)
    Abstract [en]

    Interval temporal logics take time intervals, instead of time points, as their primitive temporal entities. One of the most studied interval temporal logics is Halpern and Shoham’s modal logic of time intervals HS, which associates a modal operator with each binary relation between intervals over a linear order (the so-called Allen’s interval relations). In this paper, we compare and classify the expressiveness of all fragments of HS on the class of all linear orders and on the subclass of all dense linear orders. For each of these classes, we identify a complete set of definabilities between HS modalities, valid in that class, thus obtaining a complete classification of the family of all 4096 fragments of HS with respect to their expressiveness. We show that on the class of all linear orders there are exactly 1347 expressively different fragments of HS, while on the class of dense linear orders there are exactly 966 such expressively different fragments.

  • 2.
    Avigad, Jeremy
    et al.
    Department of Philosophy and Department of Mathematical Sciences, Carnegie Mellon University, Pittsburgh, Pennsylvania, U.S.A..
    Kapulkin, Krzysztof
    Department of Mathematics, University of Pittsburgh, Pennsylvania, U.S.A..
    Lumsdaine, Peter LeFanu
    Institute for Advanced Study, Princeton, New Jersey, U.S.A..
    Homotopy limits in type theory2015In: Mathematical Structures in Computer Science, ISSN 0960-1295, E-ISSN 1469-8072, Vol. 25, no 5, p. 1040-1070Article in journal (Refereed)
    Abstract [en]

    Working in homotopy type theory, we provide a systematic study of homotopy limits of diagrams over graphs, formalized in the Coq proof assistant. We discuss some of the challenges posed by this approach to formalizing homotopy-theoretic material. We also compare our constructions with the more classical approach to homotopy limits via fibration categories.

  • 3.
    Awodey, Steve
    Stockholm University, Faculty of Science, Department of Mathematics. Carnegie Mellon University, USA.
    A cubical model of homotopy type theory2016Report (Other academic)
  • 4.
    Backelin, Jörgen
    et al.
    Stockholm University, Faculty of Science, Department of Mathematics.
    Oneto, Alessandro
    Stockholm University, Faculty of Science, Department of Mathematics.
    On a class of power ideals2015In: Journal of Pure and Applied Algebra, ISSN 0022-4049, E-ISSN 1873-1376, Vol. 219, no 8, p. 3158-3180Article in journal (Refereed)
    Abstract [en]

    In this paper we study the class of power ideals generated by the k(n) forms (x(0) + xi(g1) x(1) + ... + xi(gn) x(n))((k-1)d) where xi is a fixed primitive kth-root of unity and 0 <= g(j) <= k - 1 for all j. For k = 2, by using a Z(k)(n+1)-grading on C[x(0),..., x(n)], we compute the Hilbert series of the associated quotient rings via a simple numerical algorithm. We also conjecture the extension for k > 2. Via Macaulay duality, those power ideals are related to schemes of fat points with support on the k(n) points [1 : xi(g1) : ... : xi(gn)] in P-n. We compute Hilbert series, Betti numbers and Grobner basis for these 0-dimensional schemes. This explicitly determines the Hilbert series of the power ideal for all k: that this agrees with our conjecture for k > 2 is supported by several computer experiments.

  • 5.
    Backman, Theo
    Stockholm University, Faculty of Science, Department of Mathematics.
    Configuration spaces, props and wheel-free deformation quantization2016Doctoral thesis, monograph (Other academic)
    Abstract [en]

    The main theme of this thesis is higher algebraic structures that come from operads and props.

    The first chapter is an introduction to the mathematical framework needed for the content of this thesis. The chapter does not contain any new results.

    The second chapter is concerned with the construction of a configuration space model for a particular 2-colored differential graded operad encoding the structure of two A algebras with two A morphisms and a homotopy between the morphisms. The cohomology of this operad is shown to be the well-known 2-colored operad encoding the structure of two associative algebras and of an associative algebra morphism between them.

    The third chapter is concerned with deformation quantization of (potentially) infinite dimensional (quasi-)Poisson manifolds. Our proof employs a variation on the transcendental methods pioneered by M. Kontsevich for the finite dimensional case. The first proof of the infinite dimensional case is due to B. Shoikhet. A key feature of the first proof is the construction of a universal L structure on formal polyvector fields. Our contribution is a simplification of B. Shoikhet proof by considering a more natural configuration space and a simpler choice of propagator. The result is also put into a natural context of the dg Lie algebras coming from graph complexes; the L structure is proved to come from a Maurer-Cartan element in the oriented graph complex.

    The fourth chapter also deals with deformation quantization of (quasi-)Poisson structures in the infinite dimensional setting. Unlike the previous chapter, the methods used here are purely algebraic. Our main theorem is the possibility to deformation quantize quasi-Poisson structures by only using perturbative methods; in contrast to the transcendental methods employed in the previous chapter. We give two proofs of the theorem via the theory of dg operads, dg properads and dg props. We show that there is a dg prop morphism from a prop governing star-products to a dg prop(erad) governing (quasi-)Poisson structures. This morphism gives a theorem about the existence of a deformation quantization of (quasi-)Poisson structure. The proof proceeds by giving an explicit deformation quantization of super-involutive Lie bialgebras and then lifting that to the dg properad governing quasi-Poisson structures. The prop governing star-products was first considered by S.A. Merkulov, but the properad governing quasi-Poisson structures is a new construction.

    The second proof of the theorem employs the Merkulov-Willwacher polydifferential functor to transfer the problem of finding a morphism of dg props to that of finding a morphism of dg operads.We construct an extension of the well known operad of A algebras such that the representations of it in V are equivalent to an A structure on V[[ħ]]. This new operad is also a minimal model of an operad that can be seen as the extension of the operad of associative algebras by a unary operation. We give an explicit map of operads from the extended associative operad to the operad we get when applying the Merkulov-Willwacher polydifferential functor to the properad of super-involutive Lie bialgebras. Lifting this map so as to go between their respective models gives a new proof of the main theorem.

  • 6.
    Balletti, Gabriele
    Stockholm University, Faculty of Science, Department of Mathematics.
    Connectivity through bounds for the Castelnuovo–Mumford regularity2017In: Journal of combinatorial theory. Series A (Print), ISSN 0097-3165, E-ISSN 1096-0899, Vol. 147, p. 46-54Article in journal (Refereed)
    Abstract [en]

    In this note we generalize and unify two results on connectivity of graphs: one by Balinsky and Barnette, one by Athanasiadis. This is done through a simple proof using commutative algebra tools. In particular we use bounds for the Castelnuovo-Mumford regularity of their Stanley-Reisner rings. As a result, if Delta is a simplicial d-pseudomanifold and s is the largest integer such that A has a missing face of size s, then the 1-skeleton of Delta is inverted right perpendicular(s)/((s+1)d)inverted left perpendicular-connected. We also show that this value is tight.

  • 7. Bauer, Andrej
    et al.
    Gross, Jason
    LeFanu Lumsdaine, Peter
    Stockholm University, Faculty of Science, Department of Mathematics.
    Shulman, Michael
    Sozeau, Matthieu
    Spitters, Bas
    The HoTT Library: A formalization of homotopy type theory in Coq2017In: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs / [ed] Yves Bertot, Viktor Vafeiadis, New York, NY, USA: Association for Computing Machinery (ACM), 2017, p. 164-172Conference paper (Refereed)
    Abstract [en]

    We report on the development of the HoTT library, a formalization of homotopy type theory in the Coq proof assistant. It formalizes most of basic homotopy type theory, including univalence, higher inductive types, and significant amounts of synthetic homotopy theory, as well as category theory and modalities. The library has been used as a basis for several independent developments. We discuss the decisions that led to the design of the library, and we comment on the interaction of homotopy type theory with recently introduced features of Coq, such as universe polymorphism and private inductive types.

  • 8.
    Berglund, Alexander
    Stockholm University, Faculty of Science, Department of Mathematics.
    Homological perturbation theory for algebras over operads2014In: Algebraic and Geometric Topology, ISSN 1472-2747, E-ISSN 1472-2739, Vol. 14, no 5, p. 2511-2548Article in journal (Refereed)
    Abstract [en]

    We extend homological perturbation theory to encompass algebraic structures governed by operads and cooperads. The main difficulty is to find a suitable notion of algebra homotopy that generalizes to algebras over operads  O . To solve this problem, we introduce thick maps of  O –algebras and special thick maps that we call pseudo-derivations that serve as appropriate generalizations of algebra homotopies for the purposes of homological perturbation theory. 

       As an application, we derive explicit formulas for transferring  Ω(C) –algebra structures along contractions, where C  is any connected cooperad in chain complexes. This specializes to transfer formulas for  O ∞  –algebras for any Koszul operad O , in particular for A ∞  –,  C ∞  –,  L ∞  – and  G ∞  –algebras. A key feature is that our formulas are expressed in terms of the compact description of  Ω(C) –algebras as coderivation differentials on cofree C –coalgebras. Moreover, we get formulas not only for the transferred structure and a structure on the inclusion, but also for structures on the projection and the homotopy

  • 9.
    Berglund, Alexander
    et al.
    Stockholm University, Faculty of Science, Department of Mathematics.
    Börjeson, Kaj
    Stockholm University, Faculty of Science, Department of Mathematics.
    Koszul A-algebras and free loop space homologyManuscript (preprint) (Other academic)
    Abstract [en]

    We introduce a notion of Koszul A-algebra that generalizes Priddy’s notion of a Koszul algebra and we use it to construct small A- algebra models for Hochschild cochains. As an application, this yields new techniques for computing free loop space homology algebras of manifolds that are either formal or coformal (over a field or over the integers). We illustrate these techniques in two examples. 

  • 10.
    Berglund, Alexander
    et al.
    Stockholm University, Faculty of Science, Department of Mathematics.
    Hess, Kathryn
    Homotopic Hopf-Galois extensions revisitedManuscript (preprint) (Other academic)
    Abstract [en]

    In this article we revisit the theory of homotopic Hopf-Galois extensions introduced in arXiv:0902.3393v2 [math.AT], in light of the homotopical Morita theory of comodules established in arXiv:1411.6517 [math.AT]. We generalize the theory to a relative framework, which we believe is new even in the classical context and which is essential for treating the Hopf-Galois correspondence in forthcoming work of the second author and Karpova. We study in detail homotopic Hopf-Galois extensions of differential graded algebras over a commutative ring, for which we establish a descent-type characterization analogous to the one Rognes provided in the context of ring spectra. An interesting feature in the differential graded setting is the close relationship between homotopic Hopf-Galois theory and Koszul duality theory. We show that nice enough principal fibrations of simplicial sets give rise to homotopic Hopf-Galois extensions in the differential graded setting, for which this Koszul duality has a familiar form.

  • 11.
    Berglund, Alexander
    et al.
    Stockholm University, Faculty of Science, Department of Mathematics.
    Hess, Kathryn
    Homotopical Morita theory for coringsManuscript (preprint) (Other academic)
    Abstract [en]

    A coring (A,C) consists of an algebra A and a coalgebra C in the monoidal category of A-bimodules. Corings and their comodules arise naturally in the study of Hopf-Galois extensions and descent theory, as well as in the study of Hopf algebroids. In this paper, we address the question of when two corings in a symmetric monoidal model category V are homotopically Morita equivalent, i.e., when their respective categories of comodules are Quillen equivalent. The category of comodules over the trivial coring (A,A) is isomorphic to the category of A-modules, so the question above englobes that of when two algebras are homotopically Morita equivalent. We discuss this special case in the first part of the paper, extending previously known results. To approach the general question, we introduce the notion of a 'braided bimodule' and show that adjunctions between A-Mod and B-Mod that lift to adjunctions between (A,C)-Comod and (B,D)-Comod correspond precisely to braided bimodules between (A,C) and (B,D). We then give criteria, in terms of homotopic descent, for when a braided bimodule induces a Quillen equivalence. In particular, we obtain criteria for when a morphism of corings induces a Quillen equivalence, providing a homotopic generalization of results by Hovey and Strickland on Morita equivalences of Hopf algebroids. To illustrate the general theory, we examine homotopical Morita theory for corings in the category of chain complexes over a commutative ring.

  • 12.
    Bergvall, Olof
    Stockholm University, Faculty of Science, Department of Mathematics.
    Cohomology of the moduli space of curves of genus three with level two structure2014Licentiate thesis, monograph (Other academic)
    Abstract [en]

    In this thesis we investigate the moduli space M3[2] of curves of genus 3 equipped with a symplectic level 2 structure. In particular, we are interested in the cohomology of this space. We obtain cohomological information by decomposing M3[2] into a disjoint union of two natural subspaces, Q[2] and H3[2], and then making S7- resp. S8-equivariantpoint counts of each of these spaces separately.

  • 13.
    Booij, Auke
    et al.
    University of Birmingham.
    Escardó, Martín
    University of Birmingham.
    Lumsdaine, Peter LeFanu
    Stockholm University, Faculty of Science, Department of Mathematics.
    Shulman, Michael
    University of San Diego.
    Parametricity, automorphisms of the universe, and excluded middleManuscript (preprint) (Other academic)
    Abstract [en]

    It is known that one can construct non-parametric functions by assuming classical axioms. Our work is a converse to that: we prove classical axioms in dependent type theory assuming specific instances of non-parametricity. We also address the interaction between classical axioms and the existence of automorphisms of a type universe. We work over intensional Martin-Löf dependent type theory, and in some results assume further principles including function extensionality, propositional extensionality, propositional truncation, and the univalence axiom.

  • 14.
    Brage, Jens
    Stockholm University, Faculty of Science, Department of Mathematics.
    A Natural Interpretation of Classical Proofs2006Doctoral thesis, monograph (Other academic)
    Abstract [en]

    In this thesis we use the syntactic-semantic method of constructive type theory to give meaning to classical logic, in particular Gentzen's LK.

    We interpret a derivation of a classical sequent as a derivation of a contradiction from the assumptions that the antecedent formulas are true and that the succedent formulas are false, where the concepts of truth and falsity are taken to conform to the corresponding constructive concepts, using function types to encode falsity. This representation brings LK to a manageable form that allows us to split the succedent rules into parts. In this way, every succedent rule gives rise to a natural deduction style introduction rule. These introduction rules, taken together with the antecedent rules adapted to natural deduction, yield a natural deduction calculus whose subsequent interpretation in constructive type theory gives meaning to classical logic.

    The Gentzen-Prawitz inversion principle holds for the introduction and elimination rules of the natural deduction calculus and allows for a corresponding notion of convertibility. We take the introduction rules to determine the meanings of the logical constants of classical logic and use the induced type-theoretic elimination rules to interpret the elimination rules of the natural deduction calculus. This produces an interpretation injective with respect to convertibility, contrary to an analogous translation into intuitionistic predicate logic.

    From the interpretation in constructive type theory and the interpretation of cut by explicit substitution, we derive a full precision contraction relation for a natural deduction version of LK. We use a term notation to formalize the contraction relation and the corresponding cut-elimination procedure.

    The interpretation can be read as a Brouwer-Heyting-Kolmogorov (BHK) semantics that justifies classical logic. The BHK semantics utilizes a notion of classical proof and a corresponding notion of classical truth akin to Kolmogorov's notion of pseudotruth. We also consider a second BHK semantics, more closely connected with Kolmogorov's double-negation translation.

    The first interpretation reinterprets the consequence relation while keeping the constructive interpretation of truth, whereas the second interpretation reinterprets the notion of truth while keeping the constructive interpretation of the consequence relation. The first and second interpretations act on derivations in much the same way as Plotkin's call-by-value and call-by-name continuation-passing-style translations, respectively.

    We conclude that classical logic can be given a constructive semantics by laying down introduction rules for the classical logical constants. This semantics constitutes a proof interpretation of classical logic.

  • 15. Bulling, Nils
    et al.
    Goranko, Valentin
    Stockholm University, Faculty of Humanities, Department of Philosophy.
    Jamroga, Wojciech
    Logics for reasoning about strategic abilities in multi-player games2015In: Models of strategic reasoning: logics, games and communities / [ed] Johan van Benthem, Sujata Ghosh, Rineke Verbrugge, Berlin: Springer, 2015, p. 93-136Chapter in book (Refereed)
    Abstract [en]

    We introduce and discuss basic concepts, ideas, and logical formalisms used for reasoning about strategic abilities in multi-player games. In particular, we present concurrent game models and the alternating time temporal logic ATL∗ and its fragment ATL. We discuss variations of the language and semantics of ATL∗ that take into account the limitations and complications arising from incomplete information, perfect or imperfect memory of players, reasoning within dynamically changing strategy contexts, or using stronger, constructive concepts of strategy. Finally, we briefly summarize some technical results regarding decision problems for some variants of ATL.

  • 16.
    Börjeson, Kaj
    Stockholm University, Faculty of Science, Department of Mathematics.
    A Algebras Derived from Associative Algebras with a Non-Derivation Differential2015In: Journal of Generalized Lie Theory and Applications, ISSN 1736-5279, E-ISSN 1736-4337, Vol. 9, no 1, article id 214Article in journal (Refereed)
    Abstract [en]

    Given an associative graded algebra equipped with a degree +1 differential delta we define an A-structure that measures the failure of delta to be a derivation. This can be seen as a non-commutative analog of generalized BV-algebras. In that spirit we introduce a notion of associative order for the operator delta and prove that it satisfies properties similar to the commutative case. In particular when it has associative order 2 the new product is a strictly associative product of degree +1 and there is compatibility between the products, similar to ordinary BV-algebras. We consider several examples of structures obtained in this way. In particular we obtain an A-structure on the bar complex of an A-algebra that is strictly associative if the original algebra is strictly associative. We also introduce strictly associative degree +1 products for any degree +1 action on a graded algebra. Moreover, an A∞-structure is constructed on the Hochschild cocomplex of an associative algebra with a non-degenerate inner product by using Connes’ B-operator.

  • 17.
    Börjeson, Kaj
    Stockholm University, Faculty of Science, Department of Mathematics.
    Free loop spaces, Koszul duality and A-infinity algebras2017Doctoral thesis, comprehensive summary (Other academic)
    Abstract [en]

    This thesis consists of four papers on the topics of free loop spaces, Koszul duality and A-algebras. 

    In Paper I we consider a definition of differential operators for noncommutative algebras. This definition is inspired by the connections between differential operators of commutative algebras, L-algebras and BV-algebras. We show that the definition is reasonable by establishing results that are analoguous to results in the commutative case. As a by-product of this definition we also obtain definitions for noncommutative versions of Gerstenhaber and BV-algebras. 

    In Paper II we calculate the free loop space homology of (n-1)-connected manifolds of dimension of at least 3n-2. The Chas-Sullivan loop product and the loop bracket are calculated. Over a field of characteristic zero the BV-operator is determined as well. Explicit expressions for the Betti numbers are also established, showing that they grow exponentially. 

    In Paper III we restrict our coefficients to a field of characteristic 2. We study the Dyer-Lashof operations that exist on free loop space homology in this case. Explicit calculations are carried out for manifolds that are connected sums of products of spheres. 

    In Paper IV we extend the Koszul duality methods used in Paper II by incorporating A-algebras and A-coalgebras. This extension of Koszul duality enables us to compute free loop space homology of manifolds that are not necessarily formal and coformal. As an example we carry out the computations for a non-formal simply connected 7-manifold. 

  • 18.
    Börjeson, Kaj
    Stockholm University, Faculty of Science, Department of Mathematics.
    Restricted Gerstenhaber algebra structure on the free loop homology of (Sn×Sn)#mManuscript (preprint) (Other academic)
    Abstract [en]

    We compute the 2-primary restricted Gerstenhaber algebra structure on the free loop homology of (Sn×Sn)#m. To this end we construct a small complex with an explicit retract from the Hochschild cohomology complex of the cohomology algebra. The methods involved are Koszul duality, PBW-bases and the perturbation lemma. 

  • 19. Carlini, Enrico
    et al.
    Oneto, Alessandro
    Stockholm University, Faculty of Science, Department of Mathematics. Polytechnic University of Turin, Italy.
    Monomials as Sums of k-th Powers of Forms2015In: Communications in Algebra, ISSN 0092-7872, E-ISSN 1532-4125, Vol. 43, no 2, p. 650-658Article in journal (Refereed)
    Abstract [en]

    Motivated by recent results on the Waring problem for polynomial rings [4] and representation of monomial as sum of powers of linear forms [3], we consider the problem of presenting monomials of degree kd as sums of kth-powers of forms of degree d. We produce a general bound on the number of summands for any number of variables which we refine in the two variables case. We completely solve the k = 3 case for monomials in two and three variables.

  • 20. Crispin Quiñonez, Veronica
    et al.
    Lundqvist, Samuel
    Stockholm University, Faculty of Science, Department of Mathematics.
    Nenashev, Gleb
    Stockholm University, Faculty of Science, Department of Mathematics.
    On ideals generated by two generic quadratic forms in the exterior algebraManuscript (preprint) (Other academic)
    Abstract [en]

    Based on the structure theory of pairs of skew-symmetric matrices, we give a conjecture for the Hilbert series of the exterior algebra modulo the ideal generated by two generic quadratic forms. We show that the conjectured series is an upper bound in the coefficient-wise sense, and we determine a majority of the coefficients. We also conjecture that the series is equal to the series of the squarefree polynomial ring modulo the ideal generated by the squares of two generic linear forms.

  • 21.
    Crossilla, Laura
    et al.
    Leeds University.
    Palmgren, Erik
    Stockholm University, Faculty of Science, Department of Mathematics.
    Schuster, Peter
    Leeds University.
    A generalized cut characterization of the fullness axiom in CZF2013In: Logic journal of the IGPL (Print), ISSN 1367-0751, E-ISSN 1368-9894, Vol. 21, no 1, p. 63-76Article in journal (Refereed)
  • 22.
    Ekdahl, Anna-Lena
    Stockholm University, Faculty of Science, Department of Mathematics and Science Education.
    Elevers skilda sätt att erfara talmönster - en studie av elever i årskurs 3 och 42012Independent thesis Advanced level (degree of Master (Two Years)), 20 credits / 30 HE creditsStudent thesis
    Abstract [sv]

    Matematiken handlar i mångt och mycket om att lösa problem och se mönster. Talmönster är en viktig del inom algebran och aritmetiken och är det fenomen som jag i denna studie vill undersöka elevers uppfattningar av. Syftet med föreliggande kvalitativa studie är att skapa kunskap om elevers skilda sätt att erfara talmönster, såväl talföljder som visuella talmönster. Därutöver syftar studien till att identifiera kritiska aspekter utifrån de skilda sätt som talmönstren erfars av eleverna.

    Nio elever i årskurs 3 och 4 har intervjuats utifrån ett antal talmönster. Fenomenografin och variationsteorin utgör studiens teoretiska utgångspunkter och har använts för att analysera materialet. I analysen har förutom likheter och skillnader mellan sätten att erfara, innehållet i elevutsagorna analyserats utifrån erfarandets referentiella och strukturella aspekt.

    Resultatet av den fenomenografiska analysen har utmynnat i följande sex beskrivningskategorier:

    Jämn förflyttning, Konstant eller icke-konstant skillnad, Kombination av delar, Relation mellan vissa delar, Olika del- och helhetsstrukturer och Utöver angiven helhet. I analysen har de aspekter som eleverna fokuserat på varit vägledande för att skilja kategorierna åt och identifiera sex kritiska aspekter. En av dessa kritiska aspekter handlar om att urskilja att förhållandet mellan delarna i mönstret kan se olika ut. En annan kritisk aspekt är fråga om att kunna urskilja delarnas inbördes relation, relationernas förhållande till helheten och den icke angivna helheten. En tredje innebär att delarna behöver urskiljas samtidigt som helheten. Inte nödvändigtvis samtliga delar, men tillräckligt många för att se en regelbundenhet.

    Studiens resultat har gett didaktiska implikationer om vad eleverna i en undervisningssituation behöver ges möjlighet att urskilja för att utveckla ett mer innehållsrikt och differentierat sätt att erfara talmönster.

    Resultatet diskuteras utifrån tidigare internationella undersökningar. Det förs även en diskussion om vad studiens resultat kan tillföra och de didaktiska implikationer resultatet ger.

  • 23.
    Emmenegger, Jacopo
    Stockholm University, Faculty of Science, Department of Mathematics.
    A category-theoretic version of the identity type weak factorization systemManuscript (preprint) (Other academic)
    Abstract [en]

    Gambino and Garner proved that the syntactic category of a dependent type theory with identity types can be endowed with a weak factorization system structure, called identity type weak factorization system. In this paper we consider an enrichment of Joyal's notion of tribe which allow us to prove a purely category-theoretic version of the identity type weak factorization system, thus generalizing Gambino and Garner's result. We investigate then how it relates with other well-known weak factorization systems, namely those arising from Quillen model structures on the category of topological spaces and on the category of small groupoids.

  • 24.
    Emmenegger, Jacopo
    Stockholm University, Faculty of Science, Department of Mathematics.
    On the local cartesian closure of exact completionsManuscript (preprint) (Other academic)
    Abstract [en]

    A characterisation of cartesian closure of exact completions as a property of the projective objects was given by Carboni and Rosolini. We show that the argument used to prove that characterisation is equivalent to the projectives being closed under binary products (equivalently, being internally projective). The property in question is the existence of weak simple products (a slight strengthening of weak exponentials) and the argument used relies on two claims: that weak simple products endow the internal logic with universal quantification, and that an exponential is the quotient of a weak exponential. We show that either these claims hold if and only if the projectives are internally projectives, which entails that Carboni and Rosolini's characterisation only applies to ex/lex completions. We then argue that this limitation depends on the universal property of weak simple products, and derive from this observation an alternative notion, which we call generalised weak simple product. We conclude by showing that existence of generalised weak simple products in the subcategory of projectives is equivalent to the cartesian closure of the exact category, thus obtaining a complete characterisation of (local) cartesian closure for exact completions of categories with weak finite limits.

  • 25.
    Emmenegger, Jacopo
    et al.
    Stockholm University, Faculty of Science, Department of Mathematics.
    Palmgren, Erik
    Stockholm University, Faculty of Science, Department of Mathematics.
    Exact completion and constructive theories of setsManuscript (preprint) (Other academic)
    Abstract [en]

    In the present paper we use the theory of exact completions to study categorical properties of small setoids in Martin-Loef type theory and, more generally, of models of the Constructive Elementary Theory of the Category of Sets, in terms of properties of their subcategories of choice objects (i.e. objects satisfying the axiom of choice). Because of these intended applications, we deal with categories that lack equalisers and just have weak ones, but whose objects can be regarded as collections of global elements. In this context, we study the internal logic of the categories involved, and employ this analysis to give a sufficient condition for the local cartesian closure of an exact completion. Finally, we apply this result to show when an exact completion produces a model of CETCS.

  • 26.
    Eriksson, Anders
    Stockholm University.
    Differential operators on some classes of rings2000Doctoral thesis, comprehensive summary (Other academic)
  • 27.
    Espíndola, Christian
    Stockholm University, Faculty of Science, Department of Mathematics.
    A short proof of Glivenko theorems for intermediate predicate logics2013In: Archive for mathematical logic, ISSN 0933-5846, E-ISSN 1432-0665, Vol. 52, no 7-8, p. 823-826Article in journal (Refereed)
    Abstract [en]

    We give a simple proof-theoretic argument showing that Glivenko’s theorem for propositional logic and its version for predicate logic follow as an easy consequence of the deduction theorem, which also proves some Glivenko type theorems relating intermediate predicate logics between intuitionistic and classical logic. We consider two schemata, the double negation shift (DNS) and the one consisting of instances of the principle of excluded middle for sentences (REM). We prove that both schemata combined derive classical logic, while each one of them provides a strictly weaker intermediate logic, and neither of them is derivable from the other. We show that over every intermediate logic there exists a maximal intermediate logic for which Glivenko’s theorem holds. We deduce as well a characterization of DNS, as the weakest (with respect to derivability) scheme that added to REM derives classical logic.

  • 28.
    Espíndola, Christian
    Stockholm University, Faculty of Science, Department of Mathematics.
    Achieving completeness: from constructive set theory to large cardinals2016Doctoral thesis, monograph (Other academic)
    Abstract [en]

    This thesis is an exploration of several completeness phenomena, both in the constructive and the classical settings. After some introductory chapters in the first part of the thesis where we outline the background used later on, the constructive part contains a categorical formulation of several constructive completeness theorems available in the literature, but presented here in an unified framework. We develop them within a constructive reverse mathematical viewpoint, highlighting the metatheory used in each case and the strength of the corresponding completeness theorems.

    The classical part of the thesis focuses on infinitary intuitionistic propositional and predicate logic. We consider a propositional axiomatic system with a special distributivity rule that is enough to prove a completeness theorem, and we introduce weakly compact cardinals as the adequate metatheoretical assumption for this development. Finally, we return to the categorical formulation focusing this time on infinitary first-order intuitionistic logic. We propose a first-order system with a special rule, transfinite transitivity, that embodies both distributivity as well as a form of dependent choice, and study the extent to which completeness theorems can be established. We prove completeness using a weakly compact cardinal, and, like in the constructive part, we study disjunction-free fragments as well. The assumption of weak compactness is shown to be essential for the completeness theorems to hold.

  • 29.
    Espíndola, Christian
    Stockholm University, Faculty of Science, Department of Mathematics.
    Semantic Completeness of First-Order Theories in Constructive Reverse Mathematics2016In: Notre Dame Journal of Formal Logic, ISSN 0029-4527, E-ISSN 1939-0726, Vol. 57, no 2, p. 281-286Article in journal (Refereed)
    Abstract [en]

    We introduce a general notion of semantic structure for first-order theories, covering a variety of constructions such as Tarski and Kripke semantics, and prove that, over Zermelo–Fraenkel set theory (ZF), the completeness of such semantics is equivalent to the Boolean prime ideal theorem (BPI). Using a result of McCarty (2008), we conclude that the completeness of Kripke semantics is equivalent, over intuitionistic Zermelo–Fraenkel set theory (IZF), to the Law of Excluded Middle plus BPI. Along the way, we also prove the equivalence, over ZF, between BPI and the completeness theorem for Kripke semantics for both first-order and propositional theories.

  • 30.
    Everitt, Tom
    et al.
    Stockholm University, Faculty of Science, Department of Mathematics.
    Lattimore, Tor
    Hutter, Marcus
    Free Lunch for Optimisation under the Universal Distribution2014In: 2014 IEEE Congress on Evolutionary Computation (CEC), New York: IEEE Computer Society, 2014, p. 167-174Conference paper (Refereed)
    Abstract [en]

    Function optimisation is a major challenge in computer science. The No Free Lunch theorems state that if all functions with the same histogram are assumed to be equally probable then no algorithm outperforms any other in expectation. We argue against the uniform assumption and suggest a universal prior exists for which there is a free lunch, but where no particular class of functions is favoured over another. We also prove upper and lower boundson the size of the free lunch.

  • 31.
    Forssell, Henrik
    et al.
    Stockholm University, Faculty of Science, Department of Mathematics. University of Oslo.
    Lumsdaine, Peter LeFanu
    Stockholm University, Faculty of Science, Department of Mathematics.
    Constructive reflection principles for regular theoriesManuscript (preprint) (Other academic)
    Abstract [en]

    Classically, any structure for a signature Σ may be completed to a model of a desired regular theory T by means of the chase construction or small object argument. Moreover, this exhibits Mod(T) as weakly reflective in Str(Σ).

    We investigate this in the constructive setting. The basic construction is unproblematic, however, it is no longer a weak reflection. Indeed, we show that various reflection principles for models of regular theories are equivalent to choice principles in the ambient set theory. However, the embedding of a structure into its chase-completion still satisfies a conservativity property, which suffices for applications such as the completeness of regular logic with respect to Tarski (i.e. set) models.

    Unlike most constructive developments of predicate logic, we do not assume that equality between symbols in the signature is decidable. While in this setting, we also give a version of one classical lemma which is trivial over discrete signatures but more interesting here: the abstraction of constants in a proof to variables.

  • 32.
    Forssell, Henrik
    et al.
    Stockholm University, Faculty of Science, Department of Mathematics.
    Robbestad Gylterud, Håkon
    Stockholm University, Faculty of Science, Department of Mathematics.
    Spivak, David I.
    Massachusetts Institute of Technology, USA.
    Type Theoretical DatabasesManuscript (preprint) (Other academic)
    Abstract [en]

    We present a soundness theorem for a dependent type theory with context constants with respect to an indexed category of (finite, abstract) simplical complexes. The point of interest for computer science is that this category can be seen to represent tables in a natural way. Thus the category is a model for databases, a single mathematical structure in which all database schemas and instances (of a suitable, but sufficiently general form) are represented. The type theory then allows for the specification of database schemas and instances, the manipulation of the same with the usual type-theoretic operations, and the posing of queries.

  • 33. Gasquet, Olivier
    et al.
    Goranko, Valentin
    Stockholm University, Faculty of Humanities, Department of Philosophy. University of Johannesburg, South Africa.
    Schwarzentruber, François
    Big Brother Logic: visual-epistemic reasoning in stationary multi-agent systems2016In: Autonomous Agents and Multi-Agent Systems, ISSN 1387-2532, E-ISSN 1573-7454, Vol. 30, no 5, p. 793-825Article in journal (Refereed)
    Abstract [en]

    We consider multi-agent scenarios where each agent controls a surveillance camera in the plane, with fixed position and angle of vision, but rotating freely. The agents can thus observe the surroundings and each other. They can also reason about each other’s observation abilities and knowledge derived from these observations. We introduce suitable logical languages for reasoning about such scenarios which involve atomic formulae stating what agents can see, multi-agent epistemic operators for individual, distributed and common knowledge, as well as dynamic operators reflecting the ability of cameras to turn around in order to reach positions satisfying formulae in the language. We also consider effects of public announcements. We introduce several different but equivalent versions of the semantics for these languages, discuss their expressiveness and provide translations in PDL style. Using these translations we develop algorithms and obtain complexity results for model checking and satisfiability testing for the basic logic BBL that we introduce here and for some of its extensions. Notably, we show that even for the extension with common knowledge, model checking and satisfiability testing remain in PSPACE. We also discuss the sensitivity of the set of validities to the admissible angles of vision of the agents’ cameras. Finally, we discuss some further extensions: adding obstacles, positioning the cameras in 3D or enabling them to change positions. Our work has potential applications to automated reasoning, formal specification and verification of observational abilities and knowledge of multi-robot systems.

  • 34.
    Goranko, Valentin
    Stockholm University, Faculty of Humanities, Department of Philosophy.
    Logic as a Tool: A Guide to Formal Logical Reasoning2016Book (Other academic)
    Abstract [en]

    The book explains the grammar, semantics and use of classical logical languages and teaches the reader how grasp the meaning and translate them to and from natural language.  It illustrates with extensive examples the use of the most popular deductive systems -- axiomatic systems, semantic tableaux, natural deduction, and resolution -- for formalising and automating logical reasoning both on propositional and on first-order level,  and provides the reader with technical skills needed for practical derivations in them.  Systematic guidelines are offered on how to perform logically correct and well-structured reasoning using these deductive systems and the reasoning techniques that they employ. 

  • 35.
    Goranko, Valentin
    et al.
    Stockholm University, Faculty of Humanities, Department of Philosophy.
    Galton, Antony
    Temporal Logic2015In: Stanford Encyclopedia of Philosophy, ISSN 1095-5054, E-ISSN 1095-5054Article in journal (Refereed)
  • 36.
    Gottlieb, Christian
    Stockholm University, Faculty of Science, Department of Mathematics.
    Finite unions of submodules2015In: Communications in Algebra, ISSN 0092-7872, E-ISSN 1532-4125, Vol. 43, no 2, p. 847-855Article in journal (Refereed)
    Abstract [en]

    This paper is concerned with finite unions of ideals and modules. The first main result is that, if N ⊆ N 1 ∪N 2 ∪ … ∪ N s is a covering of a module N by submodules N i , such that all but two of the N i are intersections of strongly irreducible modules, then N ⊆ N k for some k. The special case when N is a multiplication module is considered. The second main result generalizes earlier results on coverings by primary submodules. In the last section unions of cosets is studied.

  • 37.
    Granberg Olsson, Mattias
    Stockholm University, Faculty of Science, Department of Mathematics.
    A Model-Theoretic Proof of Gödel's Theorem: Kripke's Notion of Fulfilment2017Independent thesis Advanced level (degree of Master (Two Years)), 20 credits / 30 HE creditsStudent thesis
    Abstract [en]

    The notion of fulfilment of a formula by a sequence of numbers, an approximation of truth due to Kripke, is presented and subsequently formalised in the weak arithmetic theory IΣ1, in some detail. After a number of technical results connecting the formalised notion to the meta-theoretical one a version of Gödel’s Incompleteness Theorem, that no consistent, recursively axiomatisable, Σ2-sound extension T of Peano arithmetic is complete, is shown by construction of a true Π2-sentence and a model of T where it is false, yielding its independence from T. These results are then generalised to a more general notion of fulfilment, proving that IΣ1 has no complete, consistent, recursively axiomatisable, Σ2-sound extensions by a similar construction of an independent sentence. This generalisation comes at the cost of some naturality, however, and an explicit falsifying model will only be obtained under additional assumptions.

    The aim of the thesis is to reproduce in some detail the notions and results developed by Kripke and Quinsey and presented by Quinsey and Putnam. In particular no novel results are obtained.

  • 38. Greco, Ornella
    et al.
    Martino, Ivan
    Stockholm University, Faculty of Science, Department of Mathematics.
    Syzygies of Veronese ModulesManuscript (preprint) (Other academic)
  • 39. Hou, Kuen-Bang (Favonia)
    et al.
    Finster, Eric
    Licata, Daniel R.
    Lumsdaine, Peter LeFanu
    Stockholm University, Faculty of Science, Department of Mathematics.
    A mechanization of the Blakers-Massey connectivity theorem in Homotopy Type Theory2016In: LICS '16 Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, New York, USA: Association for Computing Machinery (ACM), 2016, p. 565-574Conference paper (Refereed)
    Abstract [en]

    This paper continues investigations in “synthetic homotopy theory”: the use of homotopy type theory to give machine-checked proofs of constructions from homotopy theory.

    We present a mechanized proof of the Blakers-Massey connectivity theorem, a result relating the higher-dimensional homotopy groups of a pushout type (roughly, a space constructed by gluing two spaces along a shared subspace) to those of the components of the pushout. This theorem gives important information about the pushout type, and has a number of useful corollaries, including the Freudenthal suspension theorem, which has been studied in previous formalizations.

    The new proof is more elementary than existing ones in abstract homotopy-theoretic settings, and the mechanization is concise and high-level, thanks to novel combinations of ideas from homotopy theory and type theory.

  • 40.
    Kapulkin, Chris
    et al.
    University of Western Ontario.
    Lumsdaine, Peter LeFanu
    Stockholm University, Faculty of Science, Department of Mathematics.
    The homotopy theory of type theoriesManuscript (preprint) (Other academic)
    Abstract [en]

    We construct a left semi-model structure on the category of intensional type theories (precisely, on CxlCat_{Id,1,Σ(,Πext)}). This presents an infinity-category of such type theories; we show moreover that there is an infinity-functor Cl_∞ from there to the infinity-category of suitably structured quasi-categories. This allows a precise formulation of the conjectures that intensional type theory gives internal languages for higher categories, and provides a framework and toolbox for further progress on these conjectures.

  • 41.
    kouri, emmi
    Stockholm University, Faculty of Science, Department of Mathematics and Science Education.
    ”Det blir lika med…”: En studie om hur elever i en årskurs 4 resonerar kring likhetstecknet2010Independent thesis Basic level (degree of Bachelor), 10 credits / 15 HE creditsStudent thesis
    Abstract [sv]

    I denna studie undersöktes hur några elever i en årskurs 4 resonerar kring likhetstecknet. Undersökningen gjordes med hjälp av kvalitativa intervjuer. Eleverna var valda och placerade på måfå i grupper där de sedan fick diskutera kring tre matematiska likheter.

    Studien visar på tendenser av relationell förståelse för likhetstecknet hos eleverna, men samtidigt problematiseras skillnaden mellan den relationella och den operationella förståelsen. Studien kommer fram till att eleverna diskuterar om uppgiftens konstiga utformning när operationen är på högra sidan av likhetstecknet och svaret är på den vänstra sidan. Eleverna hänvisar till kutym och läroböcker. Av studien framkommer det också att eleverna jämför likheterna ofta med balansvågen, både muntligt men också kroppsligt. Studien tenderar även att ge en bild av att elevers svar skiljer sig beroende på vilka uppgifterna är. 

  • 42.
    Källström, Rolf
    et al.
    University of Gävle, Department of Mathematics.
    Tadesse, Yohannes
    Stockholm University, Faculty of Science, Department of Mathematics.
    Hilbert series of modules over Lie algebroidsArticle in journal (Refereed)
    Abstract [en]

    We consider modules M over Lie algebroids g_A which are of  finite type over a local noetherian ring A.  Using ideals  J\subseteq A such that g_A . J \subseteq J  and the length  l_{g_A}(M/JM)< \infty we can define in a natural way the  Hilbert series of M with respect to the defining ideal J.  This  notion is in particular studied for modules over the Lie algebroid  of k-linear derivations g_A=T_A(I) that preserve an ideal  I\subseteq A, for example when A is the ring of convergent  power series.

  • 43. Lindström, Sten
    et al.
    Palmgren, Erik
    Stockholm University, Faculty of Science, Department of Mathematics.
    Westerståhl, Dag
    Stockholm University, Faculty of Humanities, Department of Philosophy. University of Gothenburg, Sweden.
    Introduction: The philosophy of logical consequence and inference2012In: Synthese, ISSN 0039-7857, E-ISSN 1573-0964, Vol. 187, no 3, p. 157p. 817-820Article in journal (Other academic)
  • 44.
    Loukanova, Roussanka
    Stockholm University, Faculty of Science, Department of Mathematics.
    A Formalization of Generalized Parameters in Situated Information2016In: Proceedings of the 8th International Conference on Agents and Artificial Intelligence, SciTePress, 2016, p. 343-353Conference paper (Refereed)
    Abstract [en]

    The paper introduces a higher-order, type-theoretical formal language LST GP of information content that is partial, parametric, underspecified, dependent on situations, and recursive. The terms of the formal language represent situation-theoretic objects. The language has specialized terms for constrained computations by mutual recursion. It introduces terms representing nets of parameters that are simultaneously constrained to satisfy restrictions.

  • 45.
    Loukanova, Roussanka
    Stockholm University, Faculty of Science, Department of Mathematics.
    Acyclic Recursion with Polymorphic Types and Underspecification2016In: Proceedings of the 8th International Conference on Agents and Artificial Intelligence, SciTePress, 2016, p. 392-399Conference paper (Refereed)
    Abstract [en]

    The paper extends Moschovakis higher-order type theory of acyclic recursion by adding type polymorphism. We extend the type system of the theory to model parametric information that pertains to underspecified types. Different kinds of type polymorphism are presented via type variables and recursion constructs for alternative, disjunctive type assignments. Based on the new type system, we extend the reduction calculus of the theory of acyclic recursion. We motivate the type polymorphism with examples from English language.

  • 46.
    Loukanova, Roussanka
    Stockholm University, Faculty of Science, Department of Mathematics.
    Binding Operators in Type-Theory of Algorithms for Algorithmic Binding of Functional Neuro-Receptors2017In: Proceedings of the 2017 Federated Conference on Computer Science and Information Systems / [ed] Maria Ganzha, Leszek Maciaszek, Marcin Paprzycki, Institute of Electrical and Electronics Engineers (IEEE), 2017, p. 57-66Conference paper (Refereed)
    Abstract [en]

    The paper is on a new approach to mathematics of the notion of algorithm. We extend the higher-order, type-theory of situated algorithms. The primary applications are to computational semantics of formal and natural languages and to computational neuroscience. We investigate the properties of functions and relations that bind argument slots of other functions and relations across a recursion operator acting via mutually recursive assignments.

  • 47.
    Loukanova, Roussanka
    Stockholm University, Faculty of Science, Department of Mathematics.
    Gamma-star Reduction in the Type-theory of Acyclic Algorithms2018In: Proceedings of the 10th International Conference on Agents and Artificial Intelligence (ICAART 2018) / [ed] Ana Paula Rocha, Jaap van den Herik, SciTePress, 2018, Vol. 2, p. 231-242Conference paper (Refereed)
    Abstract [en]

    The paper extends a higher-order type theory of acyclic algorithms by adding a reduction rule, which results in a stronger reduction calculus. The new reduction calculus determines a strong algorithmic equivalence between formal terms. It is very useful for simplifying terms, by eliminating sub-terms having superfluous lambda abstraction and corresponding spurious functional applications.

  • 48.
    Loukanova, Roussanka
    Stockholm University, Faculty of Science, Department of Mathematics.
    Partiality, Underspecification, Parameters and Natural Language2017In: Partiality and Underspecification in Information, Languages, and Knowledge / [ed] Henning Christiansen, M. Dolores Jiménez-López, Roussanka Loukanova, Lawrence S. Moss, Cambridge Scholars Publishing, 2017, p. 109-150Chapter in book (Refereed)
  • 49.
    Loukanova, Roussanka
    Stockholm University, Faculty of Science, Department of Mathematics.
    Typed Theory of Situated Information and its Application to Syntax-Semantics of Human Language2017In: Partiality and Underspecification in Information, Languages, and Knowledge / [ed] Henning Christiansen, M. Dolores Jiménez-López, Roussanka Loukanova, Lawrence S. Moss, Cambridge Scholars Publishing, 2017, p. 151-188Chapter in book (Refereed)
  • 50.
    Lumsdaine, Peter LeFanu
    et al.
    Institute for Advanced Study, Princeton, New Jersey, U.S.A..
    Warren, Michael A.
    Institute for Advanced Study, Princeton, New Jersey, U.S.A..
    The Local Universes Model: An Overlooked Coherence Construction for Dependent Type Theories2015In: ACM Transactions on Computational Logic, ISSN 1529-3785, E-ISSN 1557-945X, Vol. 16, no 3, article id 23Article in journal (Refereed)
    Abstract [en]

    We present a new coherence theorem for comprehension categories, providing strict models of dependent type theory with all standard constructors, including dependent products, dependent sums, identity types, and other inductive types.

    Precisely, we take as input a “weak model”: a comprehension category, equipped with structure corresponding to the desired logical constructions. We assume throughout that the base category is close to locally Cartesian closed: specifically, that products and certain exponentials exist. Beyond this, we require only that the logical structure should be weakly stable—a pure existence statement, not involving any specific choice of structure, weaker than standard categorical Beck–Chevalley conditions, and holding in the now standard homotopy-theoretic models of type theory.

    Given such a comprehension category, we construct an equivalent split one whose logical structure is strictly stable under reindexing. This yields an interpretation of type theory with the chosen constructors.

    The model is adapted from Voevodsky’s use of universes for coherence, and at the level of fibrations is a classical construction of Giraud. It may be viewed in terms of local universes or delayed substitutions. 

12 1 - 50 of 88
CiteExportLink to result list
Permanent link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf