Open Access. Powered by Scholars. Published by Universities.®
Physical Sciences and Mathematics Commons™
Open Access. Powered by Scholars. Published by Universities.®
- Keyword
-
- Air traffic management (1)
- Automated deduction (1)
- Computational geometry (1)
- Concurrent algorithms (1)
- Congressional redistricting (1)
-
- Dynamic difficulty adjustment (1)
- Enroute airspace (1)
- Evolutionary many-objective optimization (EMaO) (1)
- Evolutionary multi-objective optimization (EMO) (1)
- Flow (1)
- Formal methods (1)
- Formal systems (1)
- Gap validation (1)
- Gerrymandering (1)
- Hotspot problem (1)
- Intuitionistic logic (1)
- Mixed integer linear programming (1)
- Monte Carlo tree search (1)
- NSGA (1)
- Pareto front (1)
- Pi calculus (1)
- Process calculi (1)
- R-NSGA (1)
- Redistricting algorithms (1)
- Reinforcement learning (1)
- SAT solvers (1)
- Scheduling (1)
- Theorem provers (1)
- Type systems (1)
Articles 1 - 6 of 6
Full-Text Articles in Physical Sciences and Mathematics
Intuitr: A Theorem Prover For Intuitionistic Propositional Logic, Erik Rauer
Intuitr: A Theorem Prover For Intuitionistic Propositional Logic, Erik Rauer
Scholarly Horizons: University of Minnesota, Morris Undergraduate Journal
A constructive proof proves the existence of a mathematical object by giving the steps necessary to construct said object. Proofs of this type can be interpreted as an algorithm for creating such an object. Intuitionistic Propositional Logic (IPL) is a propositional logic system wherein all valid proofs are constructive. intuitR is a theorem prover for IPL, that is, it determines whether a given formula is valid in IPL or not. In this paper, we describe how intuitR determines the validity of a formula and review its performance. When compared on a benchmark set of problems, intuitR was determined to solve …
Filling Gaps On The Pareto Front In Multi- And Many-Objective Optimization, Richard Lussier
Filling Gaps On The Pareto Front In Multi- And Many-Objective Optimization, Richard Lussier
Scholarly Horizons: University of Minnesota, Morris Undergraduate Journal
Pareto fronts offer insight into the best found solutions of a given problem. Several algorithms have been developed to help maintain a well-distributed Pareto front and therefore offer a wide variety of solutions. However, in real-world problems, the Pareto front isn’t necessarily a continuous surface and may contain holes and/or discontinuous lines. These irregular areas on the Pareto front are considered gaps. These gaps can either be natural or artificial. In their research, Pellicer, Escudero, Alzueta, and Deb suggest a three-step procedure to find, validate, and fill these gaps. First, they developed an algorithm to generate gap points. Second, they …
Using Temporal Session Types To Analyze Time Complexities Of Concurrent Programs, Joseph M. Walbran
Using Temporal Session Types To Analyze Time Complexities Of Concurrent Programs, Joseph M. Walbran
Scholarly Horizons: University of Minnesota, Morris Undergraduate Journal
Das et al. develop a method for analyzing the time complexity of concurrent, message-passing algorithms. Their method is based on adding timing information to datatypes. Specifically, they use a family of datatypes called session types; these constrain the structure of interactions that may take place over a channel of communication. In Das’s system, the timing properties of an algorithm can be verified by a typechecker: if the timing information in the session types is mismatched, the computer will report a type error. In their paper, Das et al. develop the theory for such a typechecker, but do not provide an …
The Impact Of Dynamic Difficulty Adjustment On Player Experience In Video Games, Chineng Vang
The Impact Of Dynamic Difficulty Adjustment On Player Experience In Video Games, Chineng Vang
Scholarly Horizons: University of Minnesota, Morris Undergraduate Journal
Dynamic Difficulty Adjustment (DDA) is a process by which a video game adjusts its level of challenge to match a player’s skill level. Its popularity in the video game industry continues to grow as it has the ability to keep players continuously engaged in a game, a concept referred to as Flow. However, the influence of DDA on games has received mixed responses, specifically that it can enhance player experience as well as hinder it. This paper explores DDA through the Monte Carlo Tree Search algorithm and Reinforcement Learning, gathering feedback from players seeking to understand what about DDA is …
Scheduling Aircraft Departures To Avoid Enroute Congestion, Johannes Martinez
Scheduling Aircraft Departures To Avoid Enroute Congestion, Johannes Martinez
Scholarly Horizons: University of Minnesota, Morris Undergraduate Journal
When scheduled flights are forecast to overcrowd sections of enroute airspace, an air traffic control authority may need to delay departures. Mixed integer linear programming can be used to compute a schedule that resolves the congestion while bringing the sum of all delays to a minimum. Standard linear programming constraint formulations for such scheduling problems, however, have poor run times for instances of realistic size. A new constraint formulation based on cycles and paths through a route graph reduces run times in computational experiments. It shows particularly strong performance for schedules that approach the worst-case solution times in standard formulations.
Fighting Gerrymandering By Automating Congressional Redistricting, Jacob Jenness
Fighting Gerrymandering By Automating Congressional Redistricting, Jacob Jenness
Scholarly Horizons: University of Minnesota, Morris Undergraduate Journal
Gerrymandering is a political problem that the United States has had for more than 200 years. Politicians have taken the dull and routine process of drawing congressional districts and turned it into a highly-partisan process. However, with recent improvements in redistricting algorithms, researchers Harry Levin and Sorelle Friedler have introduced their recursive Divide and Conquer Redistricting Algorithm. This algorithm has the potential to automate the process of congressional redistricting, thereby removing the potential for bias. By utilizing a set of partitioning and swapping algorithms, the Divide and Conquer Redistricting Algorithm achieves desirable goals, such as low population deviation, and high …