Open Access. Powered by Scholars. Published by Universities.®
- Discipline
-
- Physical Sciences and Mathematics (73)
- Computer Sciences (71)
- Other Computer Sciences (66)
- Logic and Foundations (46)
- Mathematics (46)
-
- Algebra (45)
- Other Mathematics (45)
- Electrical and Computer Engineering (35)
- Other Electrical and Computer Engineering (33)
- Medicine and Health Sciences (17)
- Social and Behavioral Sciences (10)
- Psychology (7)
- Child Psychology (6)
- Hardware Systems (6)
- Arts and Humanities (5)
- Graphics and Human Computer Interfaces (5)
- Health Information Technology (5)
- Mental and Social Health (5)
- Other Mental and Social Health (5)
- Other Psychiatry and Psychology (5)
- Psychiatry and Psychology (5)
- Computer and Systems Architecture (4)
- Medical Specialties (4)
- Music (4)
- Other Rehabilitation and Therapy (4)
- Rehabilitation and Therapy (4)
- Software Engineering (4)
- Keyword
-
- Coalgebra (13)
- Modal logic (6)
- Deep learning (5)
- ADHD (4)
- Remaining useful life prediction (4)
-
- Coalgebraic logic (3)
- Coalgebras (3)
- Display calculus (3)
- Machine learning (3)
- Multiple change-point model (3)
- Virtual reality (3)
- Accessibility (2)
- Assistive technology (2)
- Autism (2)
- Autism Spectrum Disorder (2)
- Autism spectrum disorder (2)
- Behavior (2)
- Children (2)
- Computer vision (2)
- Cover modality (2)
- Degradation modeling (2)
- Descriptive general frames (2)
- Duality (2)
- Dynamic epistemic logic (2)
- Feedback control (2)
- Haptic interfaces (2)
- Inclusion (2)
- Kripke polynomial functors (2)
- Machine Learning (2)
- Modal Logic (2)
- Publication Year
- Publication
- Publication Type
Articles 31 - 60 of 96
Full-Text Articles in Other Computer Engineering
Recent Advances And Trends Of Predictive Maintenance From Data-Driven Machine Prognostics Perspective, Yuxin Wen, Md. Fashiar Rahman, Honglun Xu, Tzu-Liang Bill Tseng
Recent Advances And Trends Of Predictive Maintenance From Data-Driven Machine Prognostics Perspective, Yuxin Wen, Md. Fashiar Rahman, Honglun Xu, Tzu-Liang Bill Tseng
Engineering Faculty Articles and Research
In the Engineering discipline, prognostics play an essential role in improving system safety, reliability and enabling predictive maintenance decision-making. Due to the adoption of emerging sensing techniques and big data analytics tools, data-driven prognostic approaches are gaining popularity. This paper aims to deliver an extensive review of recent advances and trends of data-driven machine prognostics, with a focus on their applications in practice. The primary purpose of this review is to categorize existing literature and report the latest research progress and directions to support researchers and practitioners in acquiring a clear comprehension of the subject area. This paper first summarizes …
A Quantitative Validation Of Multi-Modal Image Fusion And Segmentation For Object Detection And Tracking, Nicholas Lahaye, Michael J. Garay, Brian D. Bue, Hesham El-Askary, Erik Linstead
A Quantitative Validation Of Multi-Modal Image Fusion And Segmentation For Object Detection And Tracking, Nicholas Lahaye, Michael J. Garay, Brian D. Bue, Hesham El-Askary, Erik Linstead
Mathematics, Physics, and Computer Science Faculty Articles and Research
In previous works, we have shown the efficacy of using Deep Belief Networks, paired with clustering, to identify distinct classes of objects within remotely sensed data via cluster analysis and qualitative analysis of the output data in comparison with reference data. In this paper, we quantitatively validate the methodology against datasets currently being generated and used within the remote sensing community, as well as show the capabilities and benefits of the data fusion methodologies used. The experiments run take the output of our unsupervised fusion and segmentation methodology and map them to various labeled datasets at different levels of global …
Hierarchical Scheduling For Real-Time Periodic Tasks In Symmetric Multiprocessing, Tom Springer, Peiyi Zhao
Hierarchical Scheduling For Real-Time Periodic Tasks In Symmetric Multiprocessing, Tom Springer, Peiyi Zhao
Engineering Faculty Articles and Research
In this paper, we present a new hierarchical scheduling framework for periodic tasks in symmetric multiprocessor (SMP) platforms. Partitioned and global scheduling are the two main approaches used by SMP based systems where global scheduling is recommended for overall performance and partitioned scheduling is recommended for hard real-time performance. Our approach combines both the global and partitioned approaches of traditional SMP-based schedulers to provide hard real-time performance guarantees for critical tasks and improved response times for soft real-time tasks. Implemented as part of VxWorks, the results are confirmed using a real-time benchmark application, where response times were improved for soft …
Online Laboratory Course Using Low Tech Supplies To Introduce Digital Logic Design Concepts, Dhanya Nair
Online Laboratory Course Using Low Tech Supplies To Introduce Digital Logic Design Concepts, Dhanya Nair
Engineering Faculty Articles and Research
This paper describes a Digital Logic Design Laboratory Course developed to engage students with hardware systems within an online setting. This is a junior level core course for students from Computer Science (CS), Computer Engineering (CE) and Electrical Engineering (EE). Hence, the laboratories are designed to provide the hands-on experience of breadboarding, testing and debugging essential to CE and EE while accommodating CS students with no prior hardware experience. Commercially available low-cost electronic trainers (portable workstations) are loaned to the students in addition to basic electronic components. To ensure a strong foundation in debugging, prior to utilizing these workstations, students …
On-Device Deep Learning Inference For System-On-Chip (Soc) Architectures, Tom Springer, Elia Eiroa-Lledo, Elizabeth Stevens, Erik Linstead
On-Device Deep Learning Inference For System-On-Chip (Soc) Architectures, Tom Springer, Elia Eiroa-Lledo, Elizabeth Stevens, Erik Linstead
Engineering Faculty Articles and Research
As machine learning becomes ubiquitous, the need to deploy models on real-time, embedded systems will become increasingly critical. This is especially true for deep learning solutions, whose large models pose interesting challenges for target architectures at the “edge” that are resource-constrained. The realization of machine learning, and deep learning, is being driven by the availability of specialized hardware, such as system-on-chip solutions, which provide some alleviation of constraints. Equally important, however, are the operating systems that run on this hardware, and specifically the ability to leverage commercial real-time operating systems which, unlike general purpose operating systems such as Linux, can …
Forecasting Vegetation Health In The Mena Region By Predicting Vegetation Indicators With Machine Learning Models, Sachi Perera, Wenzhao Li, Erik Linstead, Hesham El-Askary
Forecasting Vegetation Health In The Mena Region By Predicting Vegetation Indicators With Machine Learning Models, Sachi Perera, Wenzhao Li, Erik Linstead, Hesham El-Askary
Mathematics, Physics, and Computer Science Faculty Articles and Research
Machine learning (ML) techniques can be applied to predict and monitor drought conditions due to climate change. Predicting future vegetation health indicators (such as EVI, NDVI, and LAI) is one approach to forecast drought events for hotspots (e.g. Middle East and North Africa (MENA) regions). Recently, ML models were implemented to predict EVI values using parameters such as land types, time series, historical vegetation indices, land surface temperature, soil moisture, evapotranspiration etc. In this work, we collected the MODIS atmospherically corrected surface spectral reflectance imagery with multiple vegetation related indices for modeling and evaluation of drought conditions in the MENA …
Supporting Coordination Of Children With Asd Using Neurological Music Therapy: A Pilot Randomized Control Trial Comparing An Elastic Touch-Display With Tambourines, Franceli L. Cibrian, Melisa Madrigal, Marina Avelais, Monica Tentori
Supporting Coordination Of Children With Asd Using Neurological Music Therapy: A Pilot Randomized Control Trial Comparing An Elastic Touch-Display With Tambourines, Franceli L. Cibrian, Melisa Madrigal, Marina Avelais, Monica Tentori
Engineering Faculty Articles and Research
Aim
To evaluate the efficacy of Neurologic Music Therapy (NMT) using a traditional and a technological intervention (elastic touch-display) in improving the coordination of children with Autism Spectrum Disorder (ASD), as a primary outcome, and the timing and strength control of their movements as secondary outcomes.
Methods
Twenty-two children with ASD completed 8 NMT sessions, as a part of a 2-month intervention. Participants were randomly assigned to either use an elastic touch-display (experimental group) or tambourines (control group). We conducted pre- and post- assessment evaluations, including the Developmental Coordination Disorder Questionnaire (DCDQ) and motor assessments related to the control of …
A Fortran-Keras Deep Learning Bridge For Scientific Computing, Jordan Ott, Mike Pritchard, Natalie Best, Erik Linstead, Milan Curcic, Pierre Baldi
A Fortran-Keras Deep Learning Bridge For Scientific Computing, Jordan Ott, Mike Pritchard, Natalie Best, Erik Linstead, Milan Curcic, Pierre Baldi
Engineering Faculty Articles and Research
Implementing artificial neural networks is commonly achieved via high-level programming languages such as Python and easy-to-use deep learning libraries such as Keras. These software libraries come preloaded with a variety of network architectures, provide autodifferentiation, and support GPUs for fast and efficient computation. As a result, a deep learning practitioner will favor training a neural network model in Python, where these tools are readily available. However, many large-scale scientific computation projects are written in Fortran, making it difficult to integrate with modern deep learning methods. To alleviate this problem, we introduce a software library, the Fortran-Keras Bridge (FKB). This two-way …
Circus In Motion: A Multimodal Exergame Supporting Vestibular Therapy For Children With Autism, Oscar Peña, Franceli L. Cibrian, Monica Tentori
Circus In Motion: A Multimodal Exergame Supporting Vestibular Therapy For Children With Autism, Oscar Peña, Franceli L. Cibrian, Monica Tentori
Engineering Faculty Articles and Research
Exergames are serious games that involve physical exertion and are thought of as a form of exercise by using novel input models. Exergames are promising in improving the vestibular differences of children with autism but often lack of adaptation mechanisms that adjust the difficulty level of the exergame. In this paper, we present the design and development of Circus in Motion, a multimodal exergame supporting children with autism with the practice of non-locomotor movements. We describe how the data from a 3D depth camera enables the tracking of non-locomotor movements allowing children to naturally interact with the exergame . A …
Exploring The Efficacy Of Transfer Learning In Mining Image‑Based Software Artifacts, Natalie Best, Jordan Ott, Erik J. Linstead
Exploring The Efficacy Of Transfer Learning In Mining Image‑Based Software Artifacts, Natalie Best, Jordan Ott, Erik J. Linstead
Engineering Faculty Articles and Research
Background
Transfer learning allows us to train deep architectures requiring a large number of learned parameters, even if the amount of available data is limited, by leveraging existing models previously trained for another task. In previous attempts to classify image-based software artifacts in the absence of big data, it was noted that standard off-the-shelf deep architectures such as VGG could not be utilized due to their large parameter space and therefore had to be replaced by customized architectures with fewer layers. This proves to be challenging to empirical software engineers who would like to make use of existing architectures without …
Ml-Medic: A Preliminary Study Of An Interactive Visual Analysis Tool Facilitating Clinical Applications Of Machine Learning For Precision Medicine, Laura Stevens, David Kao, Jennifer Hall, Carsten Görg, Kaitlyn Abdo, Erik Linstead
Ml-Medic: A Preliminary Study Of An Interactive Visual Analysis Tool Facilitating Clinical Applications Of Machine Learning For Precision Medicine, Laura Stevens, David Kao, Jennifer Hall, Carsten Görg, Kaitlyn Abdo, Erik Linstead
Engineering Faculty Articles and Research
Accessible interactive tools that integrate machine learning methods with clinical research and reduce the programming experience required are needed to move science forward. Here, we present Machine Learning for Medical Exploration and Data-Inspired Care (ML-MEDIC), a point-and-click, interactive tool with a visual interface for facilitating machine learning and statistical analyses in clinical research. We deployed ML-MEDIC in the American Heart Association (AHA) Precision Medicine Platform to provide secure internet access and facilitate collaboration. ML-MEDIC’s efficacy for facilitating the adoption of machine learning was evaluated through two case studies in collaboration with clinical domain experts. A domain expert review was also …
Supporting Self-Regulation Of Children With Adhd Using Wearables: Tensions And Design Challenges, Franceli L. Cibrian, Kimberley D. Lakes, Arya Tavakoulnia, Kayla Guzman, Sabrina Schuck, Gillian R. Hayes
Supporting Self-Regulation Of Children With Adhd Using Wearables: Tensions And Design Challenges, Franceli L. Cibrian, Kimberley D. Lakes, Arya Tavakoulnia, Kayla Guzman, Sabrina Schuck, Gillian R. Hayes
Engineering Faculty Articles and Research
The design of wearable applications supporting children with Attention Deficit Hyperactivity Disorders (ADHD) requires a deep understanding not only of what is possible from a clinical standpoint but also how the children might understand and orient towards wearable technologies, such as a smartwatch. Through a series of participatory design workshops with children with ADHD and their caregivers, we identified tensions and challenges in designing wearable applications supporting the self-regulation of children with ADHD. In this paper, we describe the specific challenges of smartwatches for this population, the balance between self-regulation and co-regulation, and tensions when receiving notifications on a smartwatch …
Vrsensory: Designing Inclusive Virtual Games With Neurodiverse Children, Ben Wasserman, Derek Prate, Bryce Purnell, Alex Muse, Kaitlyn Abdo, Kendra Day, Louanne Boyd
Vrsensory: Designing Inclusive Virtual Games With Neurodiverse Children, Ben Wasserman, Derek Prate, Bryce Purnell, Alex Muse, Kaitlyn Abdo, Kendra Day, Louanne Boyd
Engineering Faculty Articles and Research
We explore virtual environments and accompanying interaction styles to enable inclusive play. In designing games for three neurodiverse children, we explore how designing for sensory diversity can be understood through a formal game design framework. Our process reveals that by using sensory processing needs as requirements we can make sensory and social accessible play spaces. We contribute empirical findings for accommodating sensory differences for neurodiverse children in a way that supports inclusive play. Specifically, we detail the sensory driven design choices that not only support the enjoyability of the leisure activities, but that also support the social inclusion of sensory-diverse …
Low-Energy Acceleration Of Binarized Convolutional Neural Networks Using A Spin Hall Effect Based Logic-In-Memory Architecture, Ashkan Samiee, Payal Borulkar, Ronald F. Demara, Peiyi Zhao, Yu Bai
Low-Energy Acceleration Of Binarized Convolutional Neural Networks Using A Spin Hall Effect Based Logic-In-Memory Architecture, Ashkan Samiee, Payal Borulkar, Ronald F. Demara, Peiyi Zhao, Yu Bai
Engineering Faculty Articles and Research
Deep Learning (DL) offers the advantages of high accuracy performance at tasks such as image recognition, learning of complex intelligent behaviors, and large-scale information retrieval problems such as intelligent web search. To attain the benefits of DL, the high computational and energy-consumption demands imposed by the underlying processing, interconnect, and memory devices on which software-based DL executes can benefit substantially from innovative hardware implementations. Logic-in-Memory (LIM) architectures offer potential approaches to attaining such throughput goals within area and energy constraints starting with the lowest layers of the hardware stack. In this paper, we develop a Spintronic Logic-in-Memory (S-LIM) XNOR neural …
Paper Prototyping Comfortable Vr Play For Diverse Sensory Needs, Louanne E. Boyd, Kendra Day, Ben Wasserman, Kaitlyn Abdo, Gillian Hayes, Erik J. Linstead
Paper Prototyping Comfortable Vr Play For Diverse Sensory Needs, Louanne E. Boyd, Kendra Day, Ben Wasserman, Kaitlyn Abdo, Gillian Hayes, Erik J. Linstead
Engineering Faculty Articles and Research
We co-designed paper prototype dashboards for virtual environments for three children with diverse sensory needs. Our goal was to determine individual interaction styles in order to enable comfortable and inclusive play. As a first step towards an inclusive virtual world, we began with designing for three sensory-diverse children who have labels of neurotypical, ADHD, and autism respectively. We focused on their leisure interests and their individual sensory profiles. We present the results of co-design with family members and paper prototyping sessions conducted by family members with the children. The results contribute preliminary empirical findings for accommodating different levels of engagement …
Applications Of Supervised Machine Learning In Autism Spectrum Disorder Research: A Review, Kayleigh K. Hyde, Marlena N. Novack, Nicholas Lahaye, Chelsea Parlett-Pelleriti, Raymond Anden, Dennis R. Dixon, Erik Linstead
Applications Of Supervised Machine Learning In Autism Spectrum Disorder Research: A Review, Kayleigh K. Hyde, Marlena N. Novack, Nicholas Lahaye, Chelsea Parlett-Pelleriti, Raymond Anden, Dennis R. Dixon, Erik Linstead
Engineering Faculty Articles and Research
Autism spectrum disorder (ASD) research has yet to leverage "big data" on the same scale as other fields; however, advancements in easy, affordable data collection and analysis may soon make this a reality. Indeed, there has been a notable increase in research literature evaluating the effectiveness of machine learning for diagnosing ASD, exploring its genetic underpinnings, and designing effective interventions. This paper provides a comprehensive review of 45 papers utilizing supervised machine learning in ASD, including algorithms for classification and text analysis. The goal of the paper is to identify and describe supervised machine learning trends in ASD literature as …
Exploring Age-Related Metamemory Differences Using Modified Brier Scores And Hierarchical Clustering, Chelsea Parlett-Pelleriti, Grace C. Lin, Masha R. Jones, Erik Linstead, Susanne M. Jaeggi
Exploring Age-Related Metamemory Differences Using Modified Brier Scores And Hierarchical Clustering, Chelsea Parlett-Pelleriti, Grace C. Lin, Masha R. Jones, Erik Linstead, Susanne M. Jaeggi
Engineering Faculty Articles and Research
Older adults (OAs) typically experience memory failures as they age. However, with some exceptions, studies of OAs’ ability to assess their own memory functions—Metamemory (MM)— find little evidence that this function is susceptible to age-related decline. Our study examines OAs’ and young adults’ (YAs) MM performance and strategy use. Groups of YAs (N = 138) and OAs (N = 79) performed a MM task that required participants to place bets on how likely they were to remember words in a list. Our analytical approach includes hierarchical clustering, and we introduce a new measure of MM—the modified Brier—in order to adjust …
Multiple-Change-Point Modeling And Exact Bayesian Inference Of Degradation Signal For Prognostic Improvement, Yuxin Wen, Jianguo Wu, Qiang Matthew Zhou, Tzu-Liang Bill Tseng
Multiple-Change-Point Modeling And Exact Bayesian Inference Of Degradation Signal For Prognostic Improvement, Yuxin Wen, Jianguo Wu, Qiang Matthew Zhou, Tzu-Liang Bill Tseng
Engineering Faculty Articles and Research
Prognostics play an increasingly important role in modern engineering systems for smart maintenance decision-making. In parametric regression-based approaches, the parametric models are often too rigid to model degradation signals in many applications. In this paper, we propose a Bayesian multiple-change-point (CP) modeling framework to better capture the degradation path and improve the prognostics. At the offline modeling stage, a novel stochastic process is proposed to model the joint prior of CPs and positions. All hyperparameters are estimated through an empirical two-stage process. At the online monitoring and remaining useful life (RUL) prediction stage, a recursive updating algorithm is developed to …
Investigating On Through Glass Via Based Rf Passives For 3-D Integration, Libo Qian, Jifei Sang, Yinshui Xia, Jian Wang, Peiyi Zhao
Investigating On Through Glass Via Based Rf Passives For 3-D Integration, Libo Qian, Jifei Sang, Yinshui Xia, Jian Wang, Peiyi Zhao
Mathematics, Physics, and Computer Science Faculty Articles and Research
Due to low dielectric loss and low cost, glass is developed as a promising material for advanced interposers in 2.5-D and 3-D integration. In this paper, through glass vias (TGVs) are used to implement inductors for minimal footprint and large quality factor. Based on the proposed physical structure, the impact of various process and design parameters on the electrical characteristics of TGV inductors is investigated with 3-D electromagnetic simulator HFSS. It is observed that TGV inductors have identical inductance and larger quality factor in comparison with their through silicon via counterparts. Using TGV inductors and parallel plate capacitors, a compact …
Degradation Modeling And Rul Prediction Using Wiener Process Subject To Multiple Change Points And Unit Heterogeneity, Yuxin Wen, Jianguo Wu, Devashish Das, Tzu-Liang Bill Tseng
Degradation Modeling And Rul Prediction Using Wiener Process Subject To Multiple Change Points And Unit Heterogeneity, Yuxin Wen, Jianguo Wu, Devashish Das, Tzu-Liang Bill Tseng
Engineering Faculty Articles and Research
Degradation modeling is critical for health condition monitoring and remaining useful life prediction (RUL). The prognostic accuracy highly depends on the capability of modeling the evolution of degradation signals. In many practical applications, however, the degradation signals show multiple phases, where the conventional degradation models are often inadequate. To better characterize the degradation signals of multiple-phase characteristics, we propose a multiple change-point Wiener process as a degradation model. To take into account the between-unit heterogeneity, a fully Bayesian approach is developed where all model parameters are assumed random. At the offline stage, an empirical two-stage process is proposed for model …
Multiple-Phase Modeling Of Degradation Signal For Condition Monitoring And Remaining Useful Life Prediction, Yuxin Wen, Jianguo Wu, Yuan Yuan
Multiple-Phase Modeling Of Degradation Signal For Condition Monitoring And Remaining Useful Life Prediction, Yuxin Wen, Jianguo Wu, Yuan Yuan
Engineering Faculty Articles and Research
Remaining useful life prediction plays an important role in ensuring the safety, availability, and efficiency of various engineering systems. In this paper, we propose a flexible Bayesian multiple-phase modeling approach to characterize degradation signals for prognosis. The priors are specified with a novel stochastic process and the multiple-phase model is formulated to a novel state-space model to facilitate online monitoring and prediction. A particle filtering algorithm with stratified sampling and partial Gibbs resample-move strategy is developed for online model updating and residual life prediction. The advantages of the proposed method are demonstrated through extensive numerical studies and real case studies.
Features Of Agent-Based Models, Reiko Heckel, Alexander Kurz, Edmund Chattoe-Brown
Features Of Agent-Based Models, Reiko Heckel, Alexander Kurz, Edmund Chattoe-Brown
Engineering Faculty Articles and Research
The design of agent-based models (ABMs) is often ad-hoc when it comes to defining their scope. In order for the inclusion of features such as network structure, location, or dynamic change to be justified, their role in a model should be systematically analysed. We propose a mechanism to compare and assess the impact of such features. In particular we are using techniques from software engineering and semantics to support the development and assessment of ABMs, such as graph transformations as semantic representations for agent-based models, feature diagrams to identify ingredients under consideration, and extension relations between graph transformation systems to …
Foreword: Special Issue On Coalgebraic Logic, Alexander Kurz
Foreword: Special Issue On Coalgebraic Logic, Alexander Kurz
Engineering Faculty Articles and Research
The second Dagstuhl seminar on coalgebraic logics took place from October 7-12, 2012, in the Leibniz Forschungszentrum Schloss Dagstuhl, following a successful earlier one in December 2009. From the 44 researchers who attended and the 30 talks presented, this collection highlights some of the progress that has been made in the field. We are grateful to Giuseppe Longo and his interest in a special issue in Mathematical Structures in Computer Science.
Quasivarieties And Varieties Of Ordered Algebras: Regularity And Exactness, Alexander Kurz
Quasivarieties And Varieties Of Ordered Algebras: Regularity And Exactness, Alexander Kurz
Engineering Faculty Articles and Research
We characterise quasivarieties and varieties of ordered algebras categorically in terms of regularity, exactness and the existence of a suitable generator. The notions of regularity and exactness need to be understood in the sense of category theory enriched over posets.
We also prove that finitary varieties of ordered algebras are cocompletions of their theories under sifted colimits (again, in the enriched sense).
The Positivication Of Coalgebraic Logics, Fredrik Dahlqvist, Alexander Kurz
The Positivication Of Coalgebraic Logics, Fredrik Dahlqvist, Alexander Kurz
Engineering Faculty Articles and Research
We present positive coalgebraic logic in full generality, and show how to obtain a positive coalgebraic logic from a boolean one. On the model side this involves canonically computing a endofunctor T': Pos->Pos from an endofunctor T: Set->Set, in a procedure previously defined by the second author et alii called posetification. On the syntax side, it involves canonically computing a syntax-building functor L': DL->DL from a syntax-building functor L: BA->BA, in a dual procedure which we call positivication. These operations are interesting in their own right and we explicitly compute posetifications and positivications in the case …
Multi-Type Display Calculus For Dynamic Epistemic Logic, Sabine Frittella, Giuseppe Greco, Alexander Kurz, Alessandra Palmigiano, Vlasta Sikimić
Multi-Type Display Calculus For Dynamic Epistemic Logic, Sabine Frittella, Giuseppe Greco, Alexander Kurz, Alessandra Palmigiano, Vlasta Sikimić
Engineering Faculty Articles and Research
In the present paper, we introduce a multi-type display calculus for dynamic epistemic logic, which we refer to as Dynamic Calculus. The displayapproach is suitable to modularly chart the space of dynamic epistemic logics on weaker-than-classical propositional base. The presence of types endows the language of the Dynamic Calculus with additional expressivity, allows for a smooth proof-theoretic treatment, and paves the way towards a general methodology for the design of proof systems for the generality of dynamic logics, and certainly beyond dynamic epistemic logic. We prove that the Dynamic Calculus adequately captures Baltag-Moss-Solecki’s dynamic epistemic logic, and enjoys Belnap-style cut …
Multi-Type Display Calculus For Propositional Dynamic Logic, Sabine Frittella, Giuseppe Greco, Alexander Kurz, Alessandra Palmigiano
Multi-Type Display Calculus For Propositional Dynamic Logic, Sabine Frittella, Giuseppe Greco, Alexander Kurz, Alessandra Palmigiano
Engineering Faculty Articles and Research
We introduce a multi-type display calculus for Propositional Dynamic Logic (PDL). This calculus is complete w.r.t. PDL, and enjoys Belnap-style cut-elimination and subformula property.
Tool Support For Reasoning In Display Calculi, Samuel Balco, Sabine Frittella, Giuseppe Greco, Alexander Kurz, Alessandra Palmigiano
Tool Support For Reasoning In Display Calculi, Samuel Balco, Sabine Frittella, Giuseppe Greco, Alexander Kurz, Alessandra Palmigiano
Engineering Faculty Articles and Research
We present a tool for reasoning in and about propositional sequent calculi. One aim is to support reasoning in calculi that contain a hundred rules or more, so that even relatively small pen and paper derivations become tedious and error prone. As an example, we implement the display calculus D.EAK of dynamic epistemic logic. Second, we provide embeddings of the calculus in the theorem prover Isabelle for formalising proofs about D.EAK. As a case study we show that the solution of the muddy children puzzle is derivable for any number of muddy children. Third, there is a set of meta-tools, …
Positive Fragments Of Coalgebraic Logics, Adriana Balan, Alexander Kurz, Jirí Velebil
Positive Fragments Of Coalgebraic Logics, Adriana Balan, Alexander Kurz, Jirí Velebil
Engineering Faculty Articles and Research
Positive modal logic was introduced in an influential 1995 paper of Dunn as the positive fragment of standard modal logic. His completeness result consists of an axiomatization that derives all modal formulas that are valid on all Kripke frames and are built only from atomic propositions, conjunction, disjunction, box and diamond. In this paper, we provide a coalgebraic analysis of this theorem, which not only gives a conceptual proof based on duality theory, but also generalizes Dunn's result from Kripke frames to coalgebras for weak-pullback preserving functors. To facilitate this analysis we prove a number of category theoretic results on …
Presenting Distributive Laws, Marcello M. Bonsangue, Helle H. Hansen, Alexander Kurz, Jurriaan Rot
Presenting Distributive Laws, Marcello M. Bonsangue, Helle H. Hansen, Alexander Kurz, Jurriaan Rot
Engineering Faculty Articles and Research
Distributive laws of a monad T over a functor F are categorical tools for specifying algebra-coalgebra interaction. They proved to be important for solving systems of corecursive equations, for the specification of well-behaved structural operational semantics and, more recently, also for enhancements of the bisimulation proof method. If T is a free monad, then such distributive laws correspond to simple natural transformations. However, when T is not free it can be rather difficult to prove the defining axioms of a distributive law. In this paper we describe how to obtain a distributive law for a monad with an equational presentation …