Physical Sciences and Mathematics Commons^™

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

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, …

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 …

Algorithmic Foundations Of Heuristic Search Using Higher-Order Polygon Inequalities, Newton Henry Campbell Jr.

CCE Theses and Dissertations

The shortest path problem in graphs is both a classic combinatorial optimization problem and a practical problem that admits many applications. Techniques for preprocessing a graph are useful for reducing shortest path query times. This dissertation studies the foundations of a class of algorithms that use preprocessed landmark information and the triangle inequality to guide A* search in graphs. A new heuristic is presented for solving shortest path queries that enables the use of higher order polygon inequalities. We demonstrate this capability by leveraging distance information from two landmarks when visiting a vertex as opposed to the common single landmark …

Blended Learning For Faculty Professional Development Incorporating Knowledge Management Principles, Julie E. Hewitt

CCE Theses and Dissertations

Adjunct faculty comprise a large percentage of part-time faculty for many colleges and universities today. Adjunct faculty are hired because they are experts in their content areas; however, this does not guarantee that they are skilled in effective classroom management. These instructors can become bewildered and frustrated because they lack the knowledge and skills that are needed to run an effective classroom.

While educational organizations have adopted blended learning environments as an effective delivery method for their students, this method has not gained much traction as a way to deliver instruction to their own employees. Thus, there are opportunities to …

An Empirical Study Of Authentication Methods To Secure E-Learning System Activities Against Impersonation Fraud, Shauna Beaudin

CCE Theses and Dissertations

Studies have revealed that securing Information Systems (IS) from intentional misuse is a concern among organizations today. The use of Web-based systems has grown dramatically across industries including e-commerce, e-banking, e-government, and e learning to name a few. Web-based systems provide e-services through a number of diverse activities. The demand for e-learning systems in both academic and non-academic organizations has increased the need to improve security against impersonation fraud. Although there are a number of studies focused on securing Web-based systems from Information Systems (IS) misuse, research has recognized the importance of identifying suitable levels of authenticating strength for various …

Mutable Class Design Pattern, Nikolay Malitsky

CCE Theses and Dissertations

The dissertation proposes, presents and analyzes a new design pattern, the Mutable Class pattern, to support the processing of large-scale heterogeneous data models with multiple families of algorithms. Handling data-algorithm associations represents an important topic across a variety of application domains. As a result, it has been addressed by multiple approaches, including the Visitor pattern and the aspect-oriented programming (AOP) paradigm. Existing solutions, however, bring additional constraints and issues. For example, the Visitor pattern freezes the class hierarchies of application models and the AOP-based projects, such as Spring AOP, introduce significant overhead for processing large-scale models with fine-grain objects. The …

Algorithmic Music Composition And Accompaniment Using Neural Networks, Daniel Wilton Risdon

Senior Projects Spring 2016

The goal of this project was to use neural networks as a tool for live music performance. Specifically, the intention was to adapt a preexisting neural network code library to work in Max, a visual programming language commonly used to create instruments and effects for electronic music and audio processing. This was done using ConvNetJS, a JavaScript library created by Andrej Karpathy.

Several neural network models were trained using a range of different training data, including music from various genres. The resulting neural network-based instruments were used to play brief pieces of music, which they used as input to create …

A Study Of The Success Of Group Formation In Virtual Teams Using Computer-Mediated Communications, Eliel Melón-Ramos

CCE Theses and Dissertations

In the digital domain, virtual teams within organizations and corporations are becoming common. Restructuring an organization or corporation is vital because competition and globalization are increasing. In this era of globalization, distributed working groups need to develop a competitive advantage in these ever-changing environments. Historically, teams had experienced problems stemming from geographical and temporal limitations. With the increase of technology in telecommunications, organizations are increasingly forming virtual teams, which have become critical to the survival of nearly any corporate entity.

Virtual teams have some of the same problems that regular teams have. One of the key challenges is the method …

Electronic Medical Records (Emr): An Empirical Testing Of Factors Contributing To Healthcare Professionals’ Resistance To Use Emr Systems, Emmanuel Patrick Bazile

CCE Theses and Dissertations

The benefits of using electronic medical records (EMRs) have been well documented; however, despite numerous financial benefits and cost reductions being offered by the federal government, some healthcare professionals have been reluctant to implement EMR systems. In fact, prior research provides evidence of failed EMR implementations due to resistance on the part of physicians, nurses, and clinical administrators. In 2010, only 25% of office-based physicians have basic EMR systems and only 10% have fully functional systems. One of the hindrances believed to be responsible for the slow implementation rates of EMR systems is resistance from healthcare professionals not truly convinced …

Line-Of-Sight Pursuit And Evasion Games On Polytopes In R^N, John Phillpot

HMC Senior Theses

We study single-pursuer, line-of-sight Pursuit and Evasion games in polytopes in $\mathbb{R}^n$. We develop winning Pursuer strategies for simple classes of polytopes (monotone prisms) in Rⁿ, using proven algorithms for polygons as inspiration and as subroutines. More generally, we show that any Pursuer-win polytope can be extended to a new Pursuer-win polytope in more dimensions. We also show that some more general classes of polytopes (monotone products) do not admit a deterministic winning Pursuer strategy. Though we provide bounds on which polytopes are Pursuer-win, these bounds are not tight. Closing the gap between those polytopes known to be …

Spest – A Tool For Specification-Based Testing, Corrigan Redford Johnson

Master's Theses

This thesis presents a tool for SPEcification based teSTing (SPEST). SPEST is designed to use well known practices for automated black-box testing to reduce the burden of testing on developers. The tool uses a simple formal specification language to generate highly-readable unit tests that embody best practices for thorough software testing. Because the specification language used to generate the assertions about the code can be compiled, it can also be used to ensure that documentation describing the code is maintained during development and refactoring.

The utility and effectiveness of SPEST were validated through several exper- iments conducted with students in …

Towards A New Gis Maturity Model: An Organizational Usage Perspective, Omer Abdulaziz Alrwais

CGU Theses & Dissertations

The first condition required for an Information Technology (IT) system to produce value is that it be used by its designated target group of users. Despite the prevalence of “system use” in IS literature, it has been often limited to the individual level. The organizational perspective is rarely considered. This dissertation focuses on system usage in the GIS domain through an organizational lens. GIS is a technology with the potential to transform government by enhancing business processes and providing a platform to manage spatial and non-spatial data, which is expected to result in better decision-making. However, little is known about …

Chillisource Game Engine Particle System Study, Angela Gross

Graduate Student Theses, Dissertations, & Professional Papers

The majority of modern game engines utilize intricate objects called particle systems which are a collection of many particles that together represent an object without well-defined surfaces. This thesis discusses the results of studying and stressing particle systems within ChilliSource, an open-source game engine written in C++, with the goal of understanding a complex system and exploring possible optimizations that could be made to it. The studies performed were driven by metrics generated with custom profiling classes that kept track of things like the number of particles rendered, how long the engine spent rendering particles, or even how long a …

An Indicator Of Inclusion With Applications To Computer Vision, Florentin Smarandache, Ovidiu Ilie Sandru

Branch Mathematics and Statistics Faculty and Staff Publications

In this paper we present an algorithmic process of necessary operations for the automatic movement of a predefined object from a video image in the target region of that image, intended to facilitate the implementation of specialized software applications in solving this kind of problems.