Open Access. Powered by Scholars. Published by Universities.®

Theory and Algorithms Commons

Open Access. Powered by Scholars. Published by Universities.®

1,210 Full-Text Articles 1,565 Authors 259,866 Downloads 108 Institutions

All Articles in Theory and Algorithms

Faceted Search

1,210 full-text articles. Page 1 of 42.

Strong Equivalence And Program's Structure In Arguing Essential Equivalence Between First-Order Logic Programs, Yuliya Lierler 2018 Department of Compter Science

Strong Equivalence And Program's Structure In Arguing Essential Equivalence Between First-Order Logic Programs, Yuliya Lierler

Yuliya Lierler

Answer set programming  is a prominent declarative programming paradigm used in formulating combinatorial search problems and implementing distinct knowledge representation formalisms. It is common that several related and yet substantially different answer set programs exist for a given problem. Sometimes these encodings may display significantly different performance. Uncovering precise formal links between these programs is often important and yet far from trivial. This paper claims the correctness   of a number of interesting program rewritings. Notably, they  assume  programs with variables and  such important language features as choice, disjunction, and aggregates. We showcase the utility of some considered rewritings  by using ...


Automatic Program Rewriting In Non-Ground Answer Set Programs, Nicholas Hippen, Yuliya Lierler 2018 University of Nebraska at Omaha

Automatic Program Rewriting In Non-Ground Answer Set Programs, Nicholas Hippen, Yuliya Lierler

Yuliya Lierler

Answer set programming is a popular constraint programming paradigm that has seen wide use across various industry applications. However, logic programs under answer set semantics often require careful design and nontrivial expertise from a programmer to obtain satisfactory solving times. In order to reduce this burden on a software engineer we propose an automated rewriting technique for non-ground logic programs that we implement in a system Projector. We conduct rigorous experimental analysis, which shows that applying system Projector to a logic program can improve its performance, even after significant human-performed optimizations.


Sampling Complexity Of Bosonic Random Walkers On A One-Dimensional Lattice, Gopikrishnan Muraleedharan, Akimasa Miyake, Ivan Deutsch 2018 University of New Mexico - Main Campus

Sampling Complexity Of Bosonic Random Walkers On A One-Dimensional Lattice, Gopikrishnan Muraleedharan, Akimasa Miyake, Ivan Deutsch

Shared Knowledge Conference

Computers based quantum logic are believed to solve problems faster and more efficiently than computers based on classical boolean logic. However, a large-scale universal quantum computer with error correction may not be realized in near future. But we can ask the question: can we devise a specific problem that a quantum device can solve faster than current state of the art super computers? One such problem is the so called "Boson Sampling" problem introduced by Aaronson and Arkhipov. The problem is to generate random numbers according to same distribution as the output number configurations of photons in linear optics. It ...


Genetic Algorithm Design Of Photonic Crystals For Energy-Efficient Ultrafast Laser Transmitters, Troy A. Hutchins-Delgado 2018 University of New Mexico

Genetic Algorithm Design Of Photonic Crystals For Energy-Efficient Ultrafast Laser Transmitters, Troy A. Hutchins-Delgado

Shared Knowledge Conference

Photonic crystals allow light to be controlled and manipulated such that novel photonic devices can be created. We are interested in using photonic crystals to increase the energy efficiency of our semiconductor whistle-geometry ring lasers. A photonic crystal will enable us to reduce the ring size, while maintaining confinement, thereby reducing its operating power. Photonic crystals can also exhibit slow light that will increase the interaction with the material. This will increase the gain, and therefore, lower the threshold for lasing to occur. Designing a photonic crystal for a particular application can be a challenge due to its number of ...


Sat-Based Explicit Ltlf Satisfiability Checking, Jianwen Li, Kristin Y. Rozier, Geguang Pu, Yueling Zhang, Moshe Y. Vardi 2018 Iowa State University

Sat-Based Explicit Ltlf Satisfiability Checking, Jianwen Li, Kristin Y. Rozier, Geguang Pu, Yueling Zhang, Moshe Y. Vardi

Aerospace Engineering Publications

We present here a SAT-based framework for LTLf (Linear Temporal Logic on Finite Traces) satisfiability checking. We use propositional SAT-solving techniques to construct a transition system for the input LTLf formula; satisfiability checking is then reduced to a path-search problem over this transition system. Furthermore, we introduce CDLSC (Conflict-Driven LTLf Satisfiability Checking), a novel algorithm that leverages information produced by propositional SAT solvers from both satisfiability and unsatisfiability results. Experimental evaluations show that CDLSC outperforms all other existing approaches for LTLf satisfiability checking, by demonstrating an approximate four-fold speedup compared to the second-best solver.


Smt-Based Constraint Answer Set Solver Ezsmt+ For Non-Tight Programs, Da Shen, Yuliya Lierler 2018 University of Nebraska at Omaha

Smt-Based Constraint Answer Set Solver Ezsmt+ For Non-Tight Programs, Da Shen, Yuliya Lierler

Yuliya Lierler

Constraint answer set programming integrates answer set programming with constraint processing. System Ezsmt+ is a constraint answer set programming tool that utilizes satisfiability modulo theory solvers for search. The truly unique feature of ezsmt+ is its capability to process linear as well as nonlinear constraints simultaneously containing integer and real variables.


The Chapman Bone Algorithm: A Diagnostic Alternative For The Evaluation Of Osteoporosis, Elise Levesque, Anton Ketterer, Wajiha Memon, Cameron James, Noah Barrett, Cyril Rakovski, Frank Frisch 2018 Chapman University

The Chapman Bone Algorithm: A Diagnostic Alternative For The Evaluation Of Osteoporosis, Elise Levesque, Anton Ketterer, Wajiha Memon, Cameron James, Noah Barrett, Cyril Rakovski, Frank Frisch

Mathematics, Physics, and Computer Science Faculty Articles and Research

Osteoporosis is the most common metabolic bone disease and goes largely undiagnosed throughout the world, due to the inaccessibility of DXA machines. Multivariate analyses of serum bone turnover markers were evaluated in 226 Orange County, California, residents with the intent to determine if serum osteocalcin and serum pyridinoline cross-links could be used to detect the onset of osteoporosis as effectively as a DXA scan. Descriptive analyses of the demographic and lab characteristics of the participants were performed through frequency, means and standard deviation estimations. We implemented logistic regression modeling to find the best classification algorithm for osteoporosis. All calculations and ...


Colenda @ The University Of Pennsylvania: Using A Decoupled, Pluggable Architecture For Object Processing, Kate Lynch 2018 University of Pennsylvania

Colenda @ The University Of Pennsylvania: Using A Decoupled, Pluggable Architecture For Object Processing, Kate Lynch

Scholarship at Penn Libraries

This poster details the architecture of the repository and the deliverables of the first major release of Colenda, the open-source repository software developed at Penn Libraries. Staff in Digital Library Development & Systems created Colenda, a long-term preservation ecosystem including Samvera, an open-source software framework for repository development, at its core. Colenda is a Samvera instance that provides materials-agnostic fuThis poster details the architecture of the repository and the deliverables of the first major release of Colenda, the open-source repository software developed at Penn Libraries. Staff in Digital Library Development & Systems created Colenda, a long-term preservation ecosystem including Samvera, an open-source ...


Rationality And Efficient Verifiable Computation, Matteo Campanelli 2018 The Graduate Center, City University of New York

Rationality And Efficient Verifiable Computation, Matteo Campanelli

All Dissertations, Theses, and Capstone Projects

In this thesis, we study protocols for delegating computation in a model where one of the parties is rational. In our model, a delegator outsources the computation of a function f on input x to a worker, who receives a (possibly monetary) reward. Our goal is to design very efficient delegation schemes where a worker is economically incentivized to provide the correct result f(x). In this work we strive for not relying on cryptographic assumptions, in particular our results do not require the existence of one-way functions.

We provide several results within the framework of rational proofs introduced by ...


Strong Equivalence And Conservative Extensions Hand In Hand For Arguing Correctness Of New Action Language C Formalization, Yuliya Lierler 2018 Department of Compter Science

Strong Equivalence And Conservative Extensions Hand In Hand For Arguing Correctness Of New Action Language C Formalization, Yuliya Lierler

Yuliya Lierler

Answer set programming  is a  declarative programming paradigm used in formulating combinatorial search problems and implementing distinct knowledge representation and reasoning formalisms. It is common that several related and yet substantially different answer set programs exist for a given problem. Uncovering precise formal links between these programs is often of value. This paper develops a methodology for establishing such links. This methodology relies on the notions of strong equivalence and conservative extensions and a body of earlier theoretical work related to these concepts. We use distinct answer set programming formalizations  of an action language C and a syntactically restricted action ...


High Performance Sparse Multivariate Polynomials: Fundamental Data Structures And Algorithms, Alex Brandt 2018 The University of Western Ontario

High Performance Sparse Multivariate Polynomials: Fundamental Data Structures And Algorithms, Alex Brandt

Electronic Thesis and Dissertation Repository

Polynomials may be represented sparsely in an effort to conserve memory usage and provide a succinct and natural representation. Moreover, polynomials which are themselves sparse – have very few non-zero terms – will have wasted memory and computation time if represented, and operated on, densely. This waste is exacerbated as the number of variables increases. We provide practical implementations of sparse multivariate data structures focused on data locality and cache complexity. We look to develop high-performance algorithms and implementations of fundamental polynomial operations, using these sparse data structures, such as arithmetic (addition, subtraction, multiplication, and division) and interpolation. We revisit a sparse ...


A Divide-And-Conquer Approach To Syntax-Guided Synthesis, Peiyuan Shen, Xiaokang Qiu 2018 Purdue University

A Divide-And-Conquer Approach To Syntax-Guided Synthesis, Peiyuan Shen, Xiaokang Qiu

The Summer Undergraduate Research Fellowship (SURF) Symposium

Program synthesis aims to generate programs automatically from user-provided specifications. One critical research thrust is called Syntax-Guideds Synthesis. In addition to semantic specifications, the user should also provide a syntactic template of the desired program, which helps the synthesizer reduce the search space. The traditional symbolic approaches, such as CounterExample-Guided Inductive Synthesis (CEGIS) framework, does not scale to large search spaces. The goal of this project is to explore a compositional, divide-n-conquer approach that heuristically divides the synthesis task into subtasks and solves them separately. The idea is to decompose the function to be synthesized by creating a set of ...


Expected Length Of The Longest Chain In Linear Hashing, Pongthip Srivarangkul, Hemanta K. Maji 2018 PurdueUniversity

Expected Length Of The Longest Chain In Linear Hashing, Pongthip Srivarangkul, Hemanta K. Maji

The Summer Undergraduate Research Fellowship (SURF) Symposium

Hash table with chaining is a data structure that chains objects with identical hash values together with an entry or a memory address. It works by calculating a hash value from an input then placing the input in the hash table entry. When we place two inputs in the same entry, they chain together in a linear linked list. We are interested in the expected length of the longest chain in linear hashing and methods to reduce the length because the worst-case look-up time is directly proportional to it.

The linear hash function used to calculate hash value is defined ...


Bayesian Analytical Approaches For Metabolomics : A Novel Method For Molecular Structure-Informed Metabolite Interaction Modeling, A Novel Diagnostic Model For Differentiating Myocardial Infarction Type, And Approaches For Compound Identification Given Mass Spectrometry Data., Patrick J. Trainor 2018 University of Louisville

Bayesian Analytical Approaches For Metabolomics : A Novel Method For Molecular Structure-Informed Metabolite Interaction Modeling, A Novel Diagnostic Model For Differentiating Myocardial Infarction Type, And Approaches For Compound Identification Given Mass Spectrometry Data., Patrick J. Trainor

Electronic Theses and Dissertations

Metabolomics, the study of small molecules in biological systems, has enjoyed great success in enabling researchers to examine disease-associated metabolic dysregulation and has been utilized for the discovery biomarkers of disease and phenotypic states. In spite of recent technological advances in the analytical platforms utilized in metabolomics and the proliferation of tools for the analysis of metabolomics data, significant challenges in metabolomics data analyses remain. In this dissertation, we present three of these challenges and Bayesian methodological solutions for each. In the first part we develop a new methodology to serve a basis for making higher order inferences in metabolomics ...


Data Center Application Security: Lateral Movement Detection Of Malware Using Behavioral Models, Harinder Pal Singh Bhasin, Elizabeth Ramsdell, Albert Alva, Rajiv Sreedhar, Medha Bhadkamkar 2018 Southen Methodist University, Dallas, Texas

Data Center Application Security: Lateral Movement Detection Of Malware Using Behavioral Models, Harinder Pal Singh Bhasin, Elizabeth Ramsdell, Albert Alva, Rajiv Sreedhar, Medha Bhadkamkar

SMU Data Science Review

Data center security traditionally is implemented at the external network access points, i.e., the perimeter of the data center network, and focuses on preventing malicious software from entering the data center. However, these defenses do not cover all possible entry points for malicious software, and they are not 100% effective at preventing infiltration through the connection points. Therefore, security is required within the data center to detect malicious software activity including its lateral movement within the data center. In this paper, we present a machine learning-based network traffic analysis approach to detect the lateral movement of malicious software within ...


Supervised Machine Learning Bot Detection Techniques To Identify Social Twitter Bots, Phillip George Efthimion, Scott Payne, Nicholas Proferes 2018 Southern Methodist University

Supervised Machine Learning Bot Detection Techniques To Identify Social Twitter Bots, Phillip George Efthimion, Scott Payne, Nicholas Proferes

SMU Data Science Review

In this paper, we present novel bot detection algorithms to identify Twitter bot accounts and to determine their prevalence in current online discourse. On social media, bots are ubiquitous. Bot accounts are problematic because they can manipulate information, spread misinformation, and promote unverified information, which can adversely affect public opinion on various topics, such as product sales and political campaigns. Detecting bot activity is complex because many bots are actively trying to avoid detection. We present a novel, complex machine learning algorithm utilizing a range of features including: length of user names, reposting rate, temporal patterns, sentiment expression, followers-to-friends ratio ...


Machine Learning To Predict College Course Success, Anthony R.Y. Dalton, Justin Beer, Sriharshasai Kommanapalli, James S. Lanich Ph.D. 2018 Southern Methodist University

Machine Learning To Predict College Course Success, Anthony R.Y. Dalton, Justin Beer, Sriharshasai Kommanapalli, James S. Lanich Ph.D.

SMU Data Science Review

In this paper, we present an analysis of the predictive ability of machine learning on the success of students in college courses in a California Community College. The California Legislature passed assembly bill 705 in order to place students in non-remedial coursework, based on high school transcripts, to increase college completion. We utilize machine learning methods on de-identified student high school transcript data to create predictive algorithms on whether or not the student will be successful in college-level English and Mathematics coursework. To satisfy the bill’s requirements, we first use exploratory data analysis on applicable transcript variables. Then we ...


Second-Order Know-How Strategies, Pavel Naumov, Jia Tao 2018 Lafayette College

Second-Order Know-How Strategies, Pavel Naumov, Jia Tao

Faculty Research and Reports

The fact that a coalition has a strategy does not mean that the coalition knows what the strategy is. If the coalition knows the strategy, then such a strategy is called a know-how strategy of the coalition. The paper proposes the notion of a second-order know-how strategy for the case when one coalition knows what the strategy of another coalition is. The main technical result is a sound and complete logical system describing the interplay between the distributed knowledge modality and the second-order coalition know-how modality.


A Survey Of Matrix Completion Methods For Recommendation Systems, Andy Ramlatchan, Mengyun Yang, Quan Liu, Min Li, Jianxin Wang, Yaohang Li 2018 Old Dominion University

A Survey Of Matrix Completion Methods For Recommendation Systems, Andy Ramlatchan, Mengyun Yang, Quan Liu, Min Li, Jianxin Wang, Yaohang Li

Computer Science Faculty Publications

In recent years, the recommendation systems have become increasingly popular and have been used in a broad variety of applications. Here, we investigate the matrix completion techniques for the recommendation systems that are based on collaborative filtering. The collaborative filtering problem can be viewed as predicting the favorability of a user with respect to new items of commodities. When a rating matrix is constructed with users as rows, items as columns, and entries as ratings, the collaborative filtering problem can then be modeled as a matrix completion problem by filling out the unknown elements in the rating matrix. This article ...


Smt-Based Answer Set Solver Cmodels-Diff (System Description), Da Shen, Yuliya Lierler 2018 University of Nebraska at Omaha

Smt-Based Answer Set Solver Cmodels-Diff (System Description), Da Shen, Yuliya Lierler

Yuliya Lierler

Many answer set solvers utilize Satisfiability solvers for search. SMT solvers extend Satisfiability solvers. This paper presents the CMODELS-DIFF system that uses SMT solvers to find answer sets of a logic program. Its theoretical foundation is based on Niemala's characterization of answer sets of a logic program via so called level rankings. The comparative experimental analysis demonstrates that CMODELS-DIFF is a viable answer set solver.


Digital Commons powered by bepress