-
Teaching Higher-Order Logic Using Isabelle
Authors:
Simon Tobias Lund,
Jørgen Villadsen
Abstract:
We present a formalization of higher-order logic in the Isabelle proof assistant, building directly on the foundational framework Isabelle/Pure and developed to be as small and readable as possible. It should therefore serve as a good introduction for someone looking into learning about higher-order logic and proof assistants, without having to study the much more complex Isabelle/HOL with heavier…
▽ More
We present a formalization of higher-order logic in the Isabelle proof assistant, building directly on the foundational framework Isabelle/Pure and developed to be as small and readable as possible. It should therefore serve as a good introduction for someone looking into learning about higher-order logic and proof assistants, without having to study the much more complex Isabelle/HOL with heavier automation. To showcase our development and approach we explain a sample proof, describe the axioms and rules of our higher-order logic, and discuss our experience with teaching the subject in a classroom setting.
△ Less
Submitted 8 April, 2024;
originally announced April 2024.
-
ProofBuddy: A Proof Assistant for Learning and Monitoring
Authors:
Nadine Karsten,
Frederik Krogsdal Jacobsen,
Kim Jana Eiken,
Uwe Nestmann,
Jørgen Villadsen
Abstract:
Proof competence, i.e. the ability to write and check (mathematical) proofs, is an important skill in Computer Science, but for many students it represents a difficult challenge. The main issues are the correct use of formal language and the ascertainment of whether proofs, especially the students' own, are complete and correct. Many authors have suggested using proof assistants to assist in teach…
▽ More
Proof competence, i.e. the ability to write and check (mathematical) proofs, is an important skill in Computer Science, but for many students it represents a difficult challenge. The main issues are the correct use of formal language and the ascertainment of whether proofs, especially the students' own, are complete and correct. Many authors have suggested using proof assistants to assist in teaching proof competence, but the efficacy of the approach is unclear. To improve the state of affairs, we introduce ProofBuddy: a web-based tool using the Isabelle proof assistant which enables researchers to conduct studies of the efficacy of approaches to using proof assistants in education by collecting fine-grained data about the way students interact with proof assistants. We have performed a preliminary usability study of ProofBuddy at the Technical University of Denmark.
△ Less
Submitted 14 August, 2023;
originally announced August 2023.
-
Coherent radio bursts from known M-dwarf planet host YZ Ceti
Authors:
J. Sebastian Pineda,
Jackie Villadsen
Abstract:
Observing magnetic star-planet interactions (SPI) offers promise for determining magnetic fields of exoplanets. Models of sub-Alfvénic SPI predict that terrestrial planets in close-in orbits around M~dwarfs can induce detectable stellar radio emission, manifesting as bursts of strongly polarized coherent radiation observable at specific planet orbital positions. We present 2-4 GHz detections of co…
▽ More
Observing magnetic star-planet interactions (SPI) offers promise for determining magnetic fields of exoplanets. Models of sub-Alfvénic SPI predict that terrestrial planets in close-in orbits around M~dwarfs can induce detectable stellar radio emission, manifesting as bursts of strongly polarized coherent radiation observable at specific planet orbital positions. We present 2-4 GHz detections of coherent radio bursts on the slowly-rotating M dwarf YZ Ceti, which hosts a compact system of terrestrial planets, the innermost orbiting with a 2-day period. Two coherent bursts occur at similar orbital phases of YZ Cet b, suggestive of an enhanced probability of bursts near that orbital phase. We model the system's magnetospheric environment in the context of sub-Alfvénic SPI and determine that YZ Ceti b can plausibly power the observed flux densities of the radio detections. However, we cannot rule out stellar magnetic activity, without a well characterized rate of non-planet-induced coherent radio bursts on slow rotators. YZ Ceti is therefore a candidate radio SPI system, with unique promise as a target for the long-term monitoring.
△ Less
Submitted 31 March, 2023;
originally announced April 2023.
-
On Exams with the Isabelle Proof Assistant
Authors:
Frederik Krogsdal Jacobsen,
Jørgen Villadsen
Abstract:
We present an approach for testing student learning outcomes in a course on automated reasoning using the Isabelle proof assistant. The approach allows us to test both general understanding of formal proofs in various logical proof systems and understanding of proofs in the higher-order logic of Isabelle/HOL in particular. The use of Isabelle enables almost automatic grading of large parts of the…
▽ More
We present an approach for testing student learning outcomes in a course on automated reasoning using the Isabelle proof assistant. The approach allows us to test both general understanding of formal proofs in various logical proof systems and understanding of proofs in the higher-order logic of Isabelle/HOL in particular. The use of Isabelle enables almost automatic grading of large parts of the exam. We explain our approach through a number of example problems, and explain why we believe that each of the kinds of problems we have selected are adequate measures of our intended learning outcomes. Finally, we discuss our experiences using the approach for the exam of a course on automated reasoning and suggest potential future work.
△ Less
Submitted 10 March, 2023;
originally announced March 2023.
-
Resolved imaging of an extrasolar radiation belt around an ultracool dwarf
Authors:
Melodie M. Kao,
Amy J. Mioduszewski,
Jackie Villadsen,
Evgenya L. Shkolnik
Abstract:
Radiation belts are present in all large-scale Solar System planetary magnetospheres: Earth, Jupiter, Saturn, Uranus, and Neptune. These persistent equatorial zones of trapped high energy particles up to tens of MeV can produce bright radio emission and impact the surface chemistry of close-in moons. Recent observations confirm planet-like radio emission such as aurorae from large-scale magnetosph…
▽ More
Radiation belts are present in all large-scale Solar System planetary magnetospheres: Earth, Jupiter, Saturn, Uranus, and Neptune. These persistent equatorial zones of trapped high energy particles up to tens of MeV can produce bright radio emission and impact the surface chemistry of close-in moons. Recent observations confirm planet-like radio emission such as aurorae from large-scale magnetospheric current systems on very low mass stars and brown dwarfs. These objects, collectively known as ultracool dwarfs, also exhibit quiescent radio emission hypothesized to trace stellar coronal flare activity or extrasolar radiation belt analogs. Here we present high resolution imaging of the ultracool dwarf LSR J1835+3259 demonstrating that this radio emission is spatially resolved and traces a long-lived, double-lobed, and axisymmetric structure similar in morphology to the Jovian radiation belts. Up to 18 ultracool dwarf radii separate the two lobes. This structure is stably present in three observations spanning >1 year. We infer a belt-like distribution of plasma confined by the magnetic dipole of LSR J1835+3259, and we estimate ~15 MeV electron energies that are consistent with those measured in the Jovian radiation belts. Though more precise constraints require higher frequency observations, a unified picture where radio emissions in ultracool dwarfs manifest from planet-like magnetospheric phenomena has emerged.
Submitted, under review.
△ Less
Submitted 2 March, 2023; v1 submitted 24 February, 2023;
originally announced February 2023.
-
Teaching Functional Programmers Logic and Metatheory
Authors:
Frederik Krogsdal Jacobsen,
Jørgen Villadsen
Abstract:
We present a novel approach for teaching logic and the metatheory of logic to students who have some experience with functional programming. We define concepts in logic as a series of functional programs in the language of the proof assistant Isabelle/HOL. This allows us to make notions which are often unclear in textbooks precise, to experiment with definitions by executing them, and to prove met…
▽ More
We present a novel approach for teaching logic and the metatheory of logic to students who have some experience with functional programming. We define concepts in logic as a series of functional programs in the language of the proof assistant Isabelle/HOL. This allows us to make notions which are often unclear in textbooks precise, to experiment with definitions by executing them, and to prove metatheoretical theorems in full detail. We have surveyed student perceptions of our teaching approach to determine its usefulness and found that students felt that our formalizations helped them understand concepts in logic, and that they experimented with them as a learning tool. However, the approach was not enough to make students feel confident in their abilities to design and implement their own formal systems. Further studies are needed to confirm and generalize the results of our survey, but our initial results seem promising.
△ Less
Submitted 26 July, 2022;
originally announced July 2022.
-
Constraining the Physical Properties of Stellar Coronal Mass Ejections with Coronal Dimming: Application to Far Ultraviolet Data of $ε$ Eridani
Authors:
R. O. Parke Loyd,
James Mason,
Meng **,
Evgenya L. Shkolnik,
Kevin France,
Allison Youngblood,
Jackie Villadsen,
Christian Schneider,
Adam C. Schneider,
Joseph Llama,
Tahina Ramiaramanantsoa,
Tyler Richey-Yowell
Abstract:
Coronal mass ejections (CMEs) are a prominent contributor to solar system space weather and might have impacted the Sun's early angular momentum evolution. A signal diagnostic of CMEs on the Sun is coronal dimming: a drop in coronal emission, tied to the mass of the CME, that is the direct result of removing emitting plasma from the corona. We present the results of a coronal dimming analysis of F…
▽ More
Coronal mass ejections (CMEs) are a prominent contributor to solar system space weather and might have impacted the Sun's early angular momentum evolution. A signal diagnostic of CMEs on the Sun is coronal dimming: a drop in coronal emission, tied to the mass of the CME, that is the direct result of removing emitting plasma from the corona. We present the results of a coronal dimming analysis of Fe XII 1349 A and Fe XXI 1354 A emission from $ε$ Eridani ($ε$ Eri), a young K2 dwarf, with archival far-ultraviolet observations by the Hubble Space Telescope's Cosmic Origins Spectrograph. Following a flare in February 2015, $ε$ Eri's Fe XXI emission declined by $81\pm5$%. Although enticing, a scant 3.8 min of preflare observations allows for the possibility that the Fe XXI decline was the decay of an earlier, unseen flare. Dimming nondetections following each of three prominent flares constrain the possible mass of ejected Fe XII-emitting (1 MK) plasma to less than a few $\times10^{15}$ g. This implies that CMEs ejecting this much or more 1 MK plasma occur less than a few times per day on $ε$ Eri. On the Sun, $10^{15}$ g CMEs occur once every few days. For $ε$ Eri, the mass loss rate due to CME-ejected 1 MK plasma could be $<0.6$ $\dot{M}_\odot$, well below the star's estimated 30 $\dot{M}_\odot$ mass loss rate (wind + CMEs). The order-of-magnitude formalism we developed for these mass estimates can be broadly applied to coronal dimming observations of any star.
△ Less
Submitted 13 July, 2022; v1 submitted 11 July, 2022;
originally announced July 2022.
-
SeCaV: A Sequent Calculus Verifier in Isabelle/HOL
Authors:
Asta Halkjær From,
Frederik Krogsdal Jacobsen,
Jørgen Villadsen
Abstract:
We describe SeCaV, a sequent calculus verifier for first-order logic in Isabelle/HOL, and the SeCaV Unshortener, an online tool that expands succinct derivations into the full SeCaV syntax. We leverage the power of Isabelle/HOL as a proof checker for our SeCaV derivations. The interactive features of Isabelle/HOL make our system transparent. For instance, the user can simply click on a side condit…
▽ More
We describe SeCaV, a sequent calculus verifier for first-order logic in Isabelle/HOL, and the SeCaV Unshortener, an online tool that expands succinct derivations into the full SeCaV syntax. We leverage the power of Isabelle/HOL as a proof checker for our SeCaV derivations. The interactive features of Isabelle/HOL make our system transparent. For instance, the user can simply click on a side condition to see its exact definition. Our formalized soundness and completeness proofs pertain exactly to the calculus as exposed to the user and not just to some model of our tool. Users can also write their derivations in the SeCaV Unshortener, which provides a lighter syntax, and expand them for later verification. We have used both tools in our teaching.
△ Less
Submitted 8 April, 2022;
originally announced April 2022.
-
Teaching Intuitionistic and Classical Propositional Logic Using Isabelle
Authors:
Jørgen Villadsen,
Asta Halkjær From,
Patrick Blackburn
Abstract:
We describe a natural deduction formalization of intuitionistic and classical propositional logic in the Isabelle/Pure framework. In contrast to earlier work, where we explored the pedagogical benefits of using a deep embedding approach to logical modelling, here we employ a logical framework modelling. This gives rise to simple and natural teaching examples and we report on the role it played in…
▽ More
We describe a natural deduction formalization of intuitionistic and classical propositional logic in the Isabelle/Pure framework. In contrast to earlier work, where we explored the pedagogical benefits of using a deep embedding approach to logical modelling, here we employ a logical framework modelling. This gives rise to simple and natural teaching examples and we report on the role it played in teaching our Automated Reasoning course in 2020 and 2021.
△ Less
Submitted 7 February, 2022;
originally announced February 2022.
-
Isabelle/HOL as a Meta-Language for Teaching Logic
Authors:
Asta Halkjær From,
Jørgen Villadsen,
Patrick Blackburn
Abstract:
Proof assistants are important tools for teaching logic. We support this claim by discussing three formalizations in Isabelle/HOL used in a recent course on automated reasoning. The first is a formalization of System W (a system of classical propositional logic with only two primitive symbols), the second is the Natural Deduction Assistant (NaDeA), and the third is a one-sided sequent calculus tha…
▽ More
Proof assistants are important tools for teaching logic. We support this claim by discussing three formalizations in Isabelle/HOL used in a recent course on automated reasoning. The first is a formalization of System W (a system of classical propositional logic with only two primitive symbols), the second is the Natural Deduction Assistant (NaDeA), and the third is a one-sided sequent calculus that uses our Sequent Calculus Verifier (SeCaV). We describe each formalization in turn, concentrating on how we used them in our teaching, and commenting on features that are interesting or useful from a logic education perspective. In the conclusion, we reflect on the lessons learned and where they might lead us next.
△ Less
Submitted 29 October, 2020;
originally announced October 2020.
-
GOAL-DTU: Development of Distributed Intelligence for the Multi-Agent Programming Contest
Authors:
Alexander Birch Jensen,
Jørgen Villadsen
Abstract:
We provide a brief description of the GOAL-DTU system for the agent contest, including the overall strategy and how the system is designed to apply this strategy. Our agents are implemented using the GOAL programming language. We evaluate the performance of our agents for the contest, and finally also discuss how to improve the system based on analysis of its strengths and weaknesses.
We provide a brief description of the GOAL-DTU system for the agent contest, including the overall strategy and how the system is designed to apply this strategy. Our agents are implemented using the GOAL programming language. We evaluate the performance of our agents for the contest, and finally also discuss how to improve the system based on analysis of its strengths and weaknesses.
△ Less
Submitted 11 June, 2020;
originally announced June 2020.
-
Teaching a Formalized Logical Calculus
Authors:
Asta Halkjær From,
Alexander Birch Jensen,
Anders Schlichtkrull,
Jørgen Villadsen
Abstract:
Classical first-order logic is in many ways central to work in mathematics, linguistics, computer science and artificial intelligence, so it is worthwhile to define it in full detail. We present soundness and completeness proofs of a sequent calculus for first-order logic, formalized in the interactive proof assistant Isabelle/HOL. Our formalization is based on work by Stefan Berghofer, which we h…
▽ More
Classical first-order logic is in many ways central to work in mathematics, linguistics, computer science and artificial intelligence, so it is worthwhile to define it in full detail. We present soundness and completeness proofs of a sequent calculus for first-order logic, formalized in the interactive proof assistant Isabelle/HOL. Our formalization is based on work by Stefan Berghofer, which we have since updated to use Isabelle's declarative proof style Isar (Archive of Formal Proofs, Entry FOL-Fitting, August 2007 / July 2018). We represent variables with de Bruijn indices; this makes substitution under quantifiers less intuitive for a human reader. However, the nature of natural numbers yields an elegant solution when compared to implementations of substitution using variables represented by strings. The sequent calculus considered has the special property of an always empty antecedent and a list of formulas in the succedent. We obtain the proofs of soundness and completeness for the sequent calculus as a derived result of the inverse duality of its tableau counterpart. We strive to not only present the results of the proofs of soundness and completeness, but also to provide a deep dive into a programming-like approach to the formalization of first-order logic syntax, semantics and the sequent calculus. We use the formalization in a bachelor course on logic for computer science and discuss our experiences.
△ Less
Submitted 28 February, 2020;
originally announced February 2020.
-
Differences in radio emission from similar M dwarfs in the binary system Ross 867-8
Authors:
L. H. Quiroga-Nuñez,
H. T. Intema,
J. R. Callingham,
J. Villadsen,
H. J. van Langevelde,
P. Jagannathan,
T. W. Shimwell,
E. P. Boven
Abstract:
Serendipitously, we have rediscovered radio emission from the binary system Ross 867 (M4.5V) and Ross 868 (M3.5V) while inspecting archival Giant Metrewave Radio Telescope (GMRT) observations. The binary system consists of two M-dwarf stars that share common characteristics such as spectral type, astrometric parameters, age and emission at infrared, optical and X-rays frequencies. The GMRT data at…
▽ More
Serendipitously, we have rediscovered radio emission from the binary system Ross 867 (M4.5V) and Ross 868 (M3.5V) while inspecting archival Giant Metrewave Radio Telescope (GMRT) observations. The binary system consists of two M-dwarf stars that share common characteristics such as spectral type, astrometric parameters, age and emission at infrared, optical and X-rays frequencies. The GMRT data at 610 MHz taken on July 2011 shows that the radio emission from Ross 867 is polarized and highly variable on hour time scales with a peak flux of 10.4 $\pm$ 0.7 mJy/beam. Additionally, after reviewing archival data from several observatories (VLA, GMRT, JVLA and LOFAR), we confirm that although both stars are likely coeval, only Ross 867 has been detected, while Ross 868 remains undetected at radio wavelengths. As they have a a large orbital separation, this binary stellar system provides a coeval laboratory to examine and constrain the stellar properties linked to radio activity in M dwarfs. We speculate that the observed difference in radio activity between the dwarfs could be due to vastly different magnetic field topologies or that Ross 867 has an intrinsically different dynamo.
△ Less
Submitted 4 December, 2019; v1 submitted 19 November, 2019;
originally announced November 2019.
-
Natural Deduction Assistant (NaDeA)
Authors:
Jørgen Villadsen,
Andreas Halkjær From,
Anders Schlichtkrull
Abstract:
We present the Natural Deduction Assistant (NaDeA) and discuss its advantages and disadvantages as a tool for teaching logic. NaDeA is available online and is based on a formalization of natural deduction in the Isabelle proof assistant. We first provide concise formulations of the main formalization results. We then elaborate on the prerequisites for NaDeA, in particular we describe a formalizati…
▽ More
We present the Natural Deduction Assistant (NaDeA) and discuss its advantages and disadvantages as a tool for teaching logic. NaDeA is available online and is based on a formalization of natural deduction in the Isabelle proof assistant. We first provide concise formulations of the main formalization results. We then elaborate on the prerequisites for NaDeA, in particular we describe a formalization in Isabelle of "Hilbert's Axioms" that we use as a starting point in our bachelor course on mathematical logic. We discuss a recent evaluation of NaDeA and also give an overview of the exercises in NaDeA.
△ Less
Submitted 1 April, 2019;
originally announced April 2019.
-
Students' Proof Assistant (SPA)
Authors:
Anders Schlichtkrull,
Jørgen Villadsen,
Andreas Halkjær From
Abstract:
The Students' Proof Assistant (SPA) aims to both teach how to use a proof assistant like Isabelle and also to teach how reliable proof assistants are built. Technically it is a miniature proof assistant inside the Isabelle proof assistant. In addition we conjecture that a good way to teach structured proving is with a concrete prover where the connection between semantics, proof system, and prover…
▽ More
The Students' Proof Assistant (SPA) aims to both teach how to use a proof assistant like Isabelle and also to teach how reliable proof assistants are built. Technically it is a miniature proof assistant inside the Isabelle proof assistant. In addition we conjecture that a good way to teach structured proving is with a concrete prover where the connection between semantics, proof system, and prover is clear. The proofs in Lamport's TLAPS proof assistant have a very similar structure to those in the declarative prover SPA. To illustrate this we compare a proof of Pelletier's problem 43 in TLAPS, Isabelle/Isar and SPA. We also consider Pelletier's problem 34, also known as Andrews's Challenge, where students are encouraged to develop their own justification function and thus obtain a lot of insight into the proof assistant. Although SPA is fully functional we have so far only used it in a few educational scenarios.
△ Less
Submitted 1 April, 2019;
originally announced April 2019.
-
Meter- to Millimeter Emission from Cool Stellar Systems: Latest Results, Synergies Across the Spectrum, and Outlook for the Next Decade
Authors:
Jan Forbrich,
Peter K. G. Williams,
Emily Drabek-Maunder,
Ward Howard,
Moira Jardine,
Lynn Matthews,
Sofia Moschou,
Robert Mutel,
Luis Quiroga-Nuñez,
Joseph Rodriguez,
Jackie Villadsen,
Andrew Zic,
Rachel Osten,
Edo Berger,
Manuel Güdel
Abstract:
Radio observations of cool stellar systems provide unique information on their magnetic fields, high-energy processes, and chemistry. Buoyed by powerful new instruments (e.g. ALMA, JVLA, LOFAR), advances in related fields (e.g., the Gaia astrometric revolution), and above all a renewed interest in the relevant stellar astrophysics, stellar radio astronomy is experiencing a renaissance. In this spl…
▽ More
Radio observations of cool stellar systems provide unique information on their magnetic fields, high-energy processes, and chemistry. Buoyed by powerful new instruments (e.g. ALMA, JVLA, LOFAR), advances in related fields (e.g., the Gaia astrometric revolution), and above all a renewed interest in the relevant stellar astrophysics, stellar radio astronomy is experiencing a renaissance. In this splinter session, participants took stock of the present state of stellar radio astronomy to chart a course for the field's future.
△ Less
Submitted 8 November, 2018;
originally announced November 2018.
-
Ultra-Wideband Detection of 22 Coherent Radio Bursts on M Dwarfs
Authors:
Jackie Villadsen,
Gregg Hallinan
Abstract:
Coherent radio bursts detected from M dwarfs have some analogy with solar radio bursts, but reach orders of magnitude higher luminosities. These events trace particle acceleration, powered by magnetic reconnection, shock fronts (such as formed by coronal mass ejections, CMEs), and magnetospheric currents, in some cases offering the only window into these processes in stellar atmospheres. We conduc…
▽ More
Coherent radio bursts detected from M dwarfs have some analogy with solar radio bursts, but reach orders of magnitude higher luminosities. These events trace particle acceleration, powered by magnetic reconnection, shock fronts (such as formed by coronal mass ejections, CMEs), and magnetospheric currents, in some cases offering the only window into these processes in stellar atmospheres. We conducted a 58-hour, ultra-wideband survey for coherent radio bursts on 5 active M dwarfs. We used the Karl G. Jansky Very Large Array (VLA) to observe simultaneously in three frequency bands covering a subset of 224-482 MHz and 1-6 GHz, achieving the widest fractional bandwidth to date for any observations of stellar radio bursts. We detected 22 bursts across 13 epochs, providing the first large sample of wideband dynamic spectra of stellar coherent radio bursts. The observed bursts have diverse morphology, with durations ranging from seconds to hours, but all share strong (40-100%) circular polarization. No events resemble solar Type II bursts (often associated with CMEs), but we cannot rule out the occurrence of radio-quiet stellar CMEs. The hours-long bursts are all polarized in the sense of the x-mode of the star's large-scale magnetic field, suggesting they are cyclotron maser emission from electrons accelerated in the large-scale field, analogous to auroral processes on ultracool dwarfs. The duty cycle of luminous coherent bursts peaks at 25% at 1-1.4 GHz, declining at lower and higher frequencies, indicating source regions in the low corona. At these frequencies, active M dwarfs should be the most common galactic transient source.
△ Less
Submitted 1 October, 2018;
originally announced October 2018.
-
Natural Deduction and the Isabelle Proof Assistant
Authors:
Jørgen Villadsen,
Andreas Halkjær From,
Anders Schlichtkrull
Abstract:
We describe our Natural Deduction Assistant (NaDeA) and the interfaces between the Isabelle proof assistant and NaDeA. In particular, we explain how NaDeA, using a generated prover that has been verified in Isabelle, provides feedback to the student, and also how NaDeA, for each formula proved by the student, provides a generated theorem that can be verified in Isabelle.
We describe our Natural Deduction Assistant (NaDeA) and the interfaces between the Isabelle proof assistant and NaDeA. In particular, we explain how NaDeA, using a generated prover that has been verified in Isabelle, provides feedback to the student, and also how NaDeA, for each formula proved by the student, provides a generated theorem that can be verified in Isabelle.
△ Less
Submitted 4 March, 2018;
originally announced March 2018.
-
Radio Emission from the Exoplanetary System $ε$ Eridani
Authors:
T. S. Bastian,
J. Villadsen,
A. Maps,
G. Hallinan,
A. J. Beasley
Abstract:
As part of a wider search for radio emission from nearby systems known or suspected to contain extrasolar planets $ε$ Eridani was observed by the Jansky Very Large Array (VLA) in the 2-4 GHz and 4-8 GHz frequency bands. In addition, as part of a separate survey of thermal emission from solar-like stars, $ε$ Eri was observed in the 8-12 GHz and the 12-18 GHz bands of the VLA. Quasi-steady continuum…
▽ More
As part of a wider search for radio emission from nearby systems known or suspected to contain extrasolar planets $ε$ Eridani was observed by the Jansky Very Large Array (VLA) in the 2-4 GHz and 4-8 GHz frequency bands. In addition, as part of a separate survey of thermal emission from solar-like stars, $ε$ Eri was observed in the 8-12 GHz and the 12-18 GHz bands of the VLA. Quasi-steady continuum radio emission from $ε$ Eri was detected in the three high-frequency bands at levels ranging from 67-83 $μ$Jy. No significant variability is seen in the quasi-steady emission. The emission in the 2-4 GHz emission, however, is shown to be the result of a circularly polarized (up to 50\%) radio pulse or flare of a few minutes duration that occurred at the beginning of the observation. We consider the astrometric position of the radio source in each frequency band relative to the expected position of the K2V star and the purported planet. The quasi-steady radio emission at frequencies $\ge \!8$ GHz is consistent with a stellar origin. The quality of the 4-8 GHz astrometry provides no meaningful constraint on the origin of the emission. The location of the 2-4 GHz radio pulse is $>2.5σ$ from the star yet, based on the ephemeris of Benedict et al. (2006), it is not consistent with the expected location of the planet either. If the radio pulse has a planetary origin, then either the planetary ephemeris is incorrect or the emission originates from another planet.
△ Less
Submitted 2 March, 2018; v1 submitted 21 June, 2017;
originally announced June 2017.
-
Using cm Observations to Constrain the Abundance of Very Small Dust Grains in Galactic Cold Cores
Authors:
C. T. Tibbs,
R. Paladini,
K. Cleary,
S. J. C. Muchovej,
A. M. M. Scaife,
M. A. Stevenson,
R. J. Laureijs,
N. Ysard,
K. J. B. Grainge,
Y. C. Perrott,
C. Rumsey,
J. Villadsen
Abstract:
In this analysis we illustrate how the relatively new emission mechanism known as spinning dust can be used to characterize dust grains in the interstellar medium. We demonstrate this by using spinning dust emission observations to constrain the abundance of very small dust grains (a $\lesssim$ 10nm) in a sample of Galactic cold cores. Using the physical properties of the cores in our sample as in…
▽ More
In this analysis we illustrate how the relatively new emission mechanism known as spinning dust can be used to characterize dust grains in the interstellar medium. We demonstrate this by using spinning dust emission observations to constrain the abundance of very small dust grains (a $\lesssim$ 10nm) in a sample of Galactic cold cores. Using the physical properties of the cores in our sample as inputs to a spinning dust model, we predict the expected level of emission at a wavelength of 1cm for four different very small dust grain abundances, which we constrain by comparing to 1cm CARMA observations. For all of our cores we find a depletion of very small grains, which we suggest is due to the process of grain growth. This work represents the first time that spinning dust emission has been used to constrain the physical properties of interstellar dust grains.
△ Less
Submitted 20 November, 2015;
originally announced November 2015.
-
CARMA Observations of Galactic Cold Cores: Searching for Spinning Dust Emission
Authors:
C. T. Tibbs,
R. Paladini,
K. Cleary,
S. J. C. Muchovej,
A. M. M. Scaife,
M. A. Stevenson,
R. J. Laureijs,
N. Ysard,
K. J. B. Grainge,
Y. C. Perrott,
C. Rumsey,
J. Villadsen
Abstract:
We present the first search for spinning dust emission from a sample of 34 Galactic cold cores, performed using the CARMA interferometer. For each of our cores we use photometric data from the Herschel Space Observatory to constrain N_{H}, T_{d}, n_{H}, and G_{0}. By computing the mass of the cores and comparing it to the Bonnor-Ebert mass, we determined that 29 of the 34 cores are gravitationally…
▽ More
We present the first search for spinning dust emission from a sample of 34 Galactic cold cores, performed using the CARMA interferometer. For each of our cores we use photometric data from the Herschel Space Observatory to constrain N_{H}, T_{d}, n_{H}, and G_{0}. By computing the mass of the cores and comparing it to the Bonnor-Ebert mass, we determined that 29 of the 34 cores are gravitationally unstable and undergoing collapse. In fact, we found that 6 cores are associated with at least one young stellar object, suggestive of their proto-stellar nature. By investigating the physical conditions within each core, we can shed light on the cm emission revealed (or not) by our CARMA observations. Indeed, we find that only 3 of our cores have any significant detectable cm emission. Using a spinning dust model, we predict the expected level of spinning dust emission in each core and find that for all 34 cores, the predicted level of emission is larger than the observed cm emission constrained by the CARMA observations. Moreover, even in the cores for which we do detect cm emission, we cannot, at this stage, discriminate between free-free emission from young stellar objects and spinning dust emission. We emphasise that, although the CARMA observations described in this analysis place important constraints on the presence of spinning dust in cold, dense environments, the source sample targeted by these observations is not statistically representative of the entire population of Galactic cores.
△ Less
Submitted 31 July, 2015;
originally announced July 2015.
-
NaDeA: A Natural Deduction Assistant with a Formalization in Isabelle
Authors:
Jørgen Villadsen,
Alexander Birch Jensen,
Anders Schlichtkrull
Abstract:
We present a new software tool for teaching logic based on natural deduction. Its proof system is formalized in the proof assistant Isabelle such that its definition is very precise. Soundness of the formalization has been proved in Isabelle. The tool is open source software developed in TypeScript / JavaScript and can thus be used directly in a browser without any further installation. Although d…
▽ More
We present a new software tool for teaching logic based on natural deduction. Its proof system is formalized in the proof assistant Isabelle such that its definition is very precise. Soundness of the formalization has been proved in Isabelle. The tool is open source software developed in TypeScript / JavaScript and can thus be used directly in a browser without any further installation. Although developed for undergraduate computer science students who are used to study and program concrete computer code in a programming language we consider the approach relevant for a broader audience and for other proof systems as well.
△ Less
Submitted 14 July, 2015;
originally announced July 2015.
-
Cool Stars and Space Weather
Authors:
A. A. Vidotto,
M. Jardine,
A. C. Cameron,
J. Morin,
J. Villadsen,
S. Saar,
J. Alvarado,
O. Cohen,
V. Holzwarth,
K. Poppenhaeger,
V. Reville
Abstract:
Stellar flares, winds and coronal mass ejections form the space weather. They are signatures of the magnetic activity of cool stars and, since activity varies with age, mass and rotation, the space weather that extra-solar planets experience can be very different from the one encountered by the solar system planets. How do stellar activity and magnetism influence the space weather of exoplanets or…
▽ More
Stellar flares, winds and coronal mass ejections form the space weather. They are signatures of the magnetic activity of cool stars and, since activity varies with age, mass and rotation, the space weather that extra-solar planets experience can be very different from the one encountered by the solar system planets. How do stellar activity and magnetism influence the space weather of exoplanets orbiting main-sequence stars? How do the environments surrounding exoplanets differ from those around the planets in our own solar system? How can the detailed knowledge acquired by the solar system community be applied in exoplanetary systems? How does space weather affect habitability? These were questions that were addressed in the splinter session "Cool stars and Space Weather", that took place on 9 Jun 2014, during the Cool Stars 18 meeting. In this paper, we present a summary of the contributions made to this session.
△ Less
Submitted 18 August, 2014;
originally announced August 2014.
-
First Detection of Thermal Radio Emission from Solar-Type Stars with the Karl G. Jansky Very Large Array
Authors:
Jackie Villadsen,
Gregg Hallinan,
Stephen Bourke,
Manuel Güdel,
Michael Rupen
Abstract:
We present the first detections of thermal radio emission from the atmospheres of solar-type stars τ Cet, η Cas A, and 40 Eri A. These stars all resemble the Sun in age and level of magnetic activity, as indicated by X-ray luminosity and chromospheric emission in calcium-II H and K lines. We observed these stars with the Karl G. Jansky Very Large Array with sensitivities of a few μJy at combinatio…
▽ More
We present the first detections of thermal radio emission from the atmospheres of solar-type stars τ Cet, η Cas A, and 40 Eri A. These stars all resemble the Sun in age and level of magnetic activity, as indicated by X-ray luminosity and chromospheric emission in calcium-II H and K lines. We observed these stars with the Karl G. Jansky Very Large Array with sensitivities of a few μJy at combinations of 10.0, 15.0, and 34.5 GHz. τ Cet, η Cas A, and 40 Eri A are all detected at 34.5 GHz with signal-to-noise ratios of 6.5, 5.2, and 4.5, respectively. 15.0-GHz upper limits imply a rising spectral index greater than 1.0 for τ Cet and 1.6 for η Cas A, at the 95% confidence level. The measured 34.5-GHz flux densities correspond to stellar disk-averaged brightness temperatures of roughly 10,000 K, similar to the solar brightness temperature at the same frequency. We explain this emission as optically- thick thermal free-free emission from the chromosphere, with possible contributions from coronal gyroresonance emission above active regions and coronal free-free emission. These and similar quality data on other nearby solar-type stars, when combined with ALMA observations, will enable the construction of temperature profiles of their chromospheres and lower transition regions.
△ Less
Submitted 9 May, 2014;
originally announced May 2014.
-
Multi-Agent Programming Contest 2012 - The Python-DTU Team
Authors:
Jørgen Villadsen,
Andreas Schmidt Jensen,
Mikko Berggren Ettienne,
Steen Vester,
Kenneth Balsiger Andersen,
Andreas Frøsig
Abstract:
We provide a brief description of the Python-DTU system, including the overall design, the tools and the algorithms that we plan to use in the agent contest.
We provide a brief description of the Python-DTU system, including the overall design, the tools and the algorithms that we plan to use in the agent contest.
△ Less
Submitted 1 October, 2012;
originally announced October 2012.
-
Multi-Agent Programming Contest 2011 - The Python-DTU Team
Authors:
Jørgen Villadsen,
Mikko Berggren Ettienne,
Steen Vester
Abstract:
We provide a brief description of the Python-DTU system, including the overall design, the tools and the algorithms that we plan to use in the agent contest.
We provide a brief description of the Python-DTU system, including the overall design, the tools and the algorithms that we plan to use in the agent contest.
△ Less
Submitted 1 October, 2011;
originally announced October 2011.
-
Multi-Agent Programming Contest 2010 - The Jason-DTU Team
Authors:
Jørgen Villadsen,
Niklas Skamriis Boss,
Andreas Schmidt Jensen,
Steen Vester
Abstract:
We provide a brief description of the Jason-DTU system, including the methodology, the tools and the team strategy that we plan to use in the agent contest.
We provide a brief description of the Jason-DTU system, including the methodology, the tools and the team strategy that we plan to use in the agent contest.
△ Less
Submitted 1 October, 2010;
originally announced October 2010.
-
Develo** Artificial Herders Using Jason
Authors:
Niklas Skamriis Boss,
Andreas Schmidt Jensen,
Jørgen Villadsen
Abstract:
This paper gives an overview of a proposed strategy for the "Cows and Herders" scenario given in the Multi-Agent Programming Contest 2009. The strategy is to be implemented using the Jason platform, based on the agent-oriented programming language Agent-Speak. The paper describes the agents, their goals and the strategies they should follow. The basis for the paper and for participating in the c…
▽ More
This paper gives an overview of a proposed strategy for the "Cows and Herders" scenario given in the Multi-Agent Programming Contest 2009. The strategy is to be implemented using the Jason platform, based on the agent-oriented programming language Agent-Speak. The paper describes the agents, their goals and the strategies they should follow. The basis for the paper and for participating in the contest is a new course given in spring 2009 and our main objective is to show that we are able to implement complex multi-agent systems with the knowledge gained in an introductory course on multi-agent systems.
△ Less
Submitted 31 December, 2009;
originally announced January 2010.
-
Nominalistic Logic (Extended Abstract)
Authors:
Jørgen Villadsen
Abstract:
Nominalistic Logic (NL) is a new presentation of Paul Gilmore's Intensional Type Theory (ITT) as a sequent calculus together with a succinct nominalization axiom (N) that permits names of predicates as individuals in certain cases. The logic has a flexible comprehension axiom, but no extensionality axiom and no infinity axiom, although axiom N is the key to the derivation of Peano's postulates f…
▽ More
Nominalistic Logic (NL) is a new presentation of Paul Gilmore's Intensional Type Theory (ITT) as a sequent calculus together with a succinct nominalization axiom (N) that permits names of predicates as individuals in certain cases. The logic has a flexible comprehension axiom, but no extensionality axiom and no infinity axiom, although axiom N is the key to the derivation of Peano's postulates for the natural numbers.
△ Less
Submitted 28 December, 2008;
originally announced December 2008.
-
Multi-dimensional Type Theory: Rules, Categories, and Combinators for Syntax and Semantics
Authors:
Jørgen Villadsen
Abstract:
We investigate the possibility of modelling the syntax and semantics of natural language by constraints, or rules, imposed by the multi-dimensional type theory Nabla. The only multiplicity we explicitly consider is two, namely one dimension for the syntax and one dimension for the semantics, but the general perspective is important. For example, issues of pragmatics could be handled as additiona…
▽ More
We investigate the possibility of modelling the syntax and semantics of natural language by constraints, or rules, imposed by the multi-dimensional type theory Nabla. The only multiplicity we explicitly consider is two, namely one dimension for the syntax and one dimension for the semantics, but the general perspective is important. For example, issues of pragmatics could be handled as additional dimensions.
One of the main problems addressed is the rather complicated repertoire of operations that exists besides the notion of categories in traditional Montague grammar. For the syntax we use a categorial grammar along the lines of Lambek. For the semantics we use so-called lexical and logical combinators inspired by work in natural logic. Nabla provides a concise interpretation and a sequent calculus as the basis for implementations.
△ Less
Submitted 15 August, 2004;
originally announced August 2004.
-
A Paraconsistent Higher Order Logic
Authors:
Jørgen Villadsen
Abstract:
Classical logic predicts that everything (thus nothing useful at all) follows from inconsistency. A paraconsistent logic is a logic where an inconsistency does not lead to such an explosion, and since in practice consistency is difficult to achieve there are many potential applications of paraconsistent logics in knowledge-based systems, logical semantics of natural language, etc. Higher order l…
▽ More
Classical logic predicts that everything (thus nothing useful at all) follows from inconsistency. A paraconsistent logic is a logic where an inconsistency does not lead to such an explosion, and since in practice consistency is difficult to achieve there are many potential applications of paraconsistent logics in knowledge-based systems, logical semantics of natural language, etc. Higher order logics have the advantages of being expressive and with several automated theorem provers available. Also the type system can be helpful. We present a concise description of a paraconsistent higher order logic with countable infinite indeterminacy, where each basic formula can get its own indeterminate truth value (or as we prefer: truth code). The meaning of the logical operators is new and rather different from traditional many-valued logics as well as from logics based on bilattices. The adequacy of the logic is examined by a case study in the domain of medicine. Thus we try to build a bridge between the HOL and MVL communities. A sequent calculus is proposed based on recent work by Muskens.
△ Less
Submitted 26 December, 2003; v1 submitted 25 July, 2002;
originally announced July 2002.
