Open Access. Powered by Scholars. Published by Universities.®
- Discipline
-
- Other Mathematics (14)
- Algebra (12)
- Computer Sciences (8)
- Applied Mathematics (6)
- Number Theory (6)
-
- Set Theory (6)
- Discrete Mathematics and Combinatorics (5)
- Other Computer Sciences (5)
- Algebraic Geometry (4)
- Computer Engineering (4)
- Engineering (4)
- Other Computer Engineering (4)
- Statistics and Probability (4)
- Analysis (3)
- Arts and Humanities (2)
- Education (2)
- Philosophy (2)
- Probability (2)
- Digital Communications and Networking (1)
- Economics (1)
- Higher Education (1)
- Logic and Foundations of Mathematics (1)
- Numerical Analysis and Scientific Computing (1)
- OS and Networks (1)
- Other Economics (1)
- Other Statistics and Probability (1)
- Physics (1)
- Institution
- Keyword
-
- Neutrosophic logic (5)
- Mathematics (3)
- Algorithm (2)
- Data mining (2)
- Display calculus (2)
-
- Graph theory (2)
- Information Theory (2)
- Multivariate analysis discrete multivariate modeling (2)
- Probabilistic graphical modeling (2)
- Reconstructability Analysis (2)
- Set theory (2)
- <p>Poisson processes.</p> <p>Poisson distribution.</p> <p>Sex differences in education.</p> (1)
- Algebraic structures (1)
- Almost primes (1)
- Ambiguity (1)
- Backward Induction (1)
- Bias (1)
- Bipolar fuzzy graph structure (BFGS) (1)
- Borel reducibility (1)
- Boundary map (1)
- Brain damage -- Mathematical models (1)
- Brain damage -- Medical statistics -- Analysis (1)
- Cardinal Number (1)
- Cartesian product (1)
- Category Theory (1)
- Choice Functions (1)
- Composition (1)
- Conditional probability (1)
- Cross product (1)
- Data analysis (1)
- Publication
-
- Branch Mathematics and Statistics Faculty and Staff Publications (12)
- Engineering Faculty Articles and Research (3)
- Applications and Applied Mathematics: An International Journal (AAM) (2)
- Systems Science Faculty Publications and Presentations (2)
- Boise State University Theses and Dissertations (1)
-
- Dissertations, Theses, and Capstone Projects (1)
- MPP Published Research (1)
- Mathematics, Physics, and Computer Science Faculty Articles and Research (1)
- OSSA Conference Archive (1)
- Publications and Research (1)
- Robert Milnikel (1)
- STAR Program Research Presentations (1)
- Senior Projects Spring 2016 (1)
- The Research and Scholarship Symposium (2013-2019) (1)
- Theses, Dissertations and Capstones (1)
- Publication Type
- File Type
Articles 1 - 30 of 30
Full-Text Articles in Logic and Foundations
Reduction Of A Nilpotent Intuitionistic Fuzzy Matrix Using Implication Operator, Riyaz A. Padder, P. Murugadas
Reduction Of A Nilpotent Intuitionistic Fuzzy Matrix Using Implication Operator, Riyaz A. Padder, P. Murugadas
Applications and Applied Mathematics: An International Journal (AAM)
A problem of reducing intuitionistic fuzzy matrices is examined and some useful properties are obtained with respect to nilpotent intutionistic fuzzy matrices. First, reduction of irreflexive and transitive intuitionistic fuzzy matrices are considered, and then the properties are applied to nilpotent intutionistic fuzzy matrices. Nilpotent intuitionistic fuzzy matrices are intuitionistic fuzzy matrices which signify acyclic graphs, and the graphs are used to characterize consistent systems. The properties are handy for generalization of various systems with intuitionistic fuzzy transitivity.
Secondary Analysis Of Concussion Data, Martin Zwick, Stephanie Kolakowsky-Hayner, Nancy Carney, Maya Balamane, Tracie Nettleton, D. Wright
Secondary Analysis Of Concussion Data, Martin Zwick, Stephanie Kolakowsky-Hayner, Nancy Carney, Maya Balamane, Tracie Nettleton, D. Wright
Systems Science Faculty Publications and Presentations
Clinical studies are expensive & time-consuming. Typically in these studies specific hypotheses are subjected to confirmatory test. Yet the data may harbor evidence of unanticipated relations between variables. It is thus desirable to subject the data to secondary analyses in the hope of discovering novel & valuable associations. Exploratory analysis, however, is tentative: findings should be replicated in new data. This presentation reports some secondary analyses on concussion data. Data mining on 2 datasets will be discussed, & some unexpected findings reported. The analyses use reconstructability analysis (RA), a probabilistic graphical modeling method implemented in the Occam software package developed …
Computation Of Shortest Path Problem In A Network With Sv-Trapezoidal Neutrosophic Numbers, Florentin Smarandache, Said Broumi, Assia Bakali, Mohamed Talea, Luige Vladareanu
Computation Of Shortest Path Problem In A Network With Sv-Trapezoidal Neutrosophic Numbers, Florentin Smarandache, Said Broumi, Assia Bakali, Mohamed Talea, Luige Vladareanu
Branch Mathematics and Statistics Faculty and Staff Publications
In this work, a neutrosophic network method is proposed for finding the shortest path length with single valued trapezoidal neutrosophic number. The proposed algorithm gives the shortest path length using score function from source node to destination node. Here the weights of the edges are considered to be single valued trapezoidal neutrosophic number. Finally, a numerical example is used to illustrate the efficiency of the proposed approach
Exploring Mathematical Strategies For Finding Hidden Features In Multi-Dimensional Big Datasets, Tri Duong, Fang Ren, Apurva Mehta
Exploring Mathematical Strategies For Finding Hidden Features In Multi-Dimensional Big Datasets, Tri Duong, Fang Ren, Apurva Mehta
STAR Program Research Presentations
With advances in technology in brighter sources and larger and faster detectors, the amount of data generated at national user facilities such as SLAC is increasing exponentially. Humans have a superb ability to recognize patterns in complex and noisy data and therefore, data is still curated and analyzed by humans. However, a human brain is unable to keep up with the accelerated pace of data generation, and as a consequence, the rate of new discoveries hasn't kept pace with the rate of data creation. Therefore, new procedures to quickly assess and analyze the data are needed. Machine learning approaches are …
Exploratory Modeling Of Tbi Data, Martin Zwick, Stephanie Kolakowsky-Hayner, Sadie Carney, Maya Balamane, Tracie Nettleton, D. Wright
Exploratory Modeling Of Tbi Data, Martin Zwick, Stephanie Kolakowsky-Hayner, Sadie Carney, Maya Balamane, Tracie Nettleton, D. Wright
Systems Science Faculty Publications and Presentations
Most data analyses are confirmatory, but exploratory studies can find unexpected non-linear & many-variable interaction effects. The methodology of reconstructability analysis (RA) is explicitly designed for exploratory modeling. It analyzes both nominal and continuous (binned) variables, is easily interpretable, takes standard text input, is web-accessible, and is available for research use. This presentation reports some results of applying RA to data sets from Preece (auto accidents) and Wright (auto/motorcycle/bike accidents, hit pedestrians, and falls).
Kolmogorov’S Axioms For Probabilities With Values In Hyperbolic Numbers, Daniel Alpay, M. E. Luna-Elizarrarás, Michael Shapiro
Kolmogorov’S Axioms For Probabilities With Values In Hyperbolic Numbers, Daniel Alpay, M. E. Luna-Elizarrarás, Michael Shapiro
Mathematics, Physics, and Computer Science Faculty Articles and Research
We introduce the notion of a probabilistic measure which takes values in hyperbolic numbers and which satisfies the system of axioms generalizing directly Kolmogorov’s system of axioms. We show that this new measure verifies the usual properties of a probability; in particular, we treat the conditional hyperbolic probability and we prove the hyperbolic analogues of the multiplication theorem, of the law of total probability and of Bayes’ theorem. Our probability may take values which are zero–divisors and we discuss carefully this peculiarity.
Certain Operations On Bipolar Fuzzy Graph Structures, Muhammad Akram, Rabia Akmal
Certain Operations On Bipolar Fuzzy Graph Structures, Muhammad Akram, Rabia Akmal
Applications and Applied Mathematics: An International Journal (AAM)
A graph structure is a useful tool in solving the combinatorial problems in different areas of computer science and computational intelligence systems. A bipolar fuzzy graph structure is a generalization of a bipolar fuzzy graph. In this paper, we present several different types of operations, including composition, Cartesian product, strong product, cross product, and lexicographic product on bipolar fuzzy graph structures. We also investigate some properties of operations.
The Logic Of Uncertain Justifications, Robert Milnikel
The Logic Of Uncertain Justifications, Robert Milnikel
Robert Milnikel
No abstract provided.
Exploring Argumentation, Objectivity, And Bias: The Case Of Mathematical Infinity, Ami Mamolo
Exploring Argumentation, Objectivity, And Bias: The Case Of Mathematical Infinity, Ami Mamolo
OSSA Conference Archive
This paper presents an overview of several years of my research into individuals’ reasoning, argumentation, and bias when addressing problems, scenarios, and symbols related to mathematical infinity. There is a long history of debate around what constitutes “objective truth” in the realm of mathematical infinity, dating back to ancient Greece (e.g., Dubinsky et al., 2005). Modes of argumentation, hindrances, and intuitions have been largely consistent over the years and across levels of expertise (e.g., Brown et al., 2010; Fischbein et al., 1979, Tsamir, 1999). This presentation examines the interrelated complexities of notions of objectivity, bias, and argumentation as manifested in …
Set-Theoretic Mereology, Joel David Hamkins, Makoto Kikuchi
Set-Theoretic Mereology, Joel David Hamkins, Makoto Kikuchi
Publications and Research
We consider a set-theoretic version of mereology based on the inclusion relation ⊆ and analyze how well it might serve as a foundation of mathematics. After establishing the non-definability of ∈ from ⊆, we identify the natural axioms for ⊆-based mereology, which constitute a finitely axiomatizable, complete, decidable theory. Ultimately, for these reasons, we conclude that this form of set-theoretic mereology cannot by itself serve as a foundation of mathematics. Meanwhile, augmented forms of set-theoretic mereology, such as that obtained by adding the singleton operator, are foundationally robust.
On The Conjugacy Problem For Automorphisms Of Trees, Kyle Douglas Beserra
On The Conjugacy Problem For Automorphisms Of Trees, Kyle Douglas Beserra
Boise State University Theses and Dissertations
In this thesis we identify the complexity of the conjugacy problem of automorphisms of regular trees. We expand on the results of Kechris, Louveau, and Friedman on the complexities of the isomorphism problem of classes of countable trees. We see in nearly all cases that the complexity of isomorphism of subtrees of a given regular countable tree is the same as the complexity of conjugacy of automorphisms of the same tree, though we present an example for which this does not hold.
On A Multiple-Choice Guessing Game, Ryan Cushman, Adam J. Hammett
On A Multiple-Choice Guessing Game, Ryan Cushman, Adam J. Hammett
The Research and Scholarship Symposium (2013-2019)
We consider the following game (a generalization of a binary version explored by Hammett and Oman): the first player (“Ann”) chooses a (uniformly) random integer from the first n positive integers, which is not revealed to the second player (“Gus”). Then, Gus presents Ann with a k-option multiple choice question concerning the number she chose, to which Ann truthfully replies. After a predetermined number m of these questions have been asked, Gus attempts to guess the number chosen by Ann. Gus wins if he guesses Ann’s number. Our goal is to determine every m-question algorithm which maximizes the probability of …
Epistemic Considerations On Extensive-Form Games, Cagil Tasdemir
Epistemic Considerations On Extensive-Form Games, Cagil Tasdemir
Dissertations, Theses, and Capstone Projects
In this thesis, we study several topics in extensive-form games. First, we consider perfect information games with belief revision with players who are tolerant of each other’s hypothetical errors. We bound the number of hypothetical non-rational moves of a player that will be tolerated by other players without revising the belief on that player’s rationality on future moves, and investigate which games yield the backward induction solution.
Second, we consider players who have no way of assigning probabilities to various possible outcomes, and define players as conservative, moderate and aggressive depending on the way they choose, and show that all …
Abstraction And Epistemic Economy, Marco Panza
Abstraction And Epistemic Economy, Marco Panza
MPP Published Research
Most of the arguments usually appealed to in order to support the view that some abstraction principles are analytic depend on ascribing to them some sort of existential parsimony or ontological neutrality, whereas the opposite arguments, aiming to deny this view, contend this ascription. As a result, other virtues that these principles might have are often overlooked. Among them, there is an epistemic virtue which I take these principles to have, when regarded in the appropriate settings, and which I suggest to call ‘epistemic economy’. My purpose is to isolate and clarify this notion by appealing to some examples concerning …
A Generalization Of The Difference Of Slopes Test To Poisson Regression With Three-Way Interaction, Melinda Bierhals
A Generalization Of The Difference Of Slopes Test To Poisson Regression With Three-Way Interaction, Melinda Bierhals
Theses, Dissertations and Capstones
Linear regression models involving interaction can use the difference of slopes test to compare slopes for various situations. We will be generalizing this process to develop a procedure to compare rates in a Poisson regression model, allowing us to consider unbounded count data as opposed to continuous data. We will apply this process to an educational data set from a sample of students located in two different Los Angeles high schools. Our model will include a three-way interaction and address the following questions:
• Does language ability impact the relationship between math ability and attendance in the same way for …
Constructing A Categorical Framework Of Metamathematical Comparison Between Deductive Systems Of Logic, Alex Gabriel Goodlad
Constructing A Categorical Framework Of Metamathematical Comparison Between Deductive Systems Of Logic, Alex Gabriel Goodlad
Senior Projects Spring 2016
The topic of this paper in a broad phrase is “proof theory". It tries to theorize the general
notion of “proving" something using rigorous definitions, inspired by previous less general
theories. The purpose for being this general is to eventually establish a rigorous framework
that can bridge the gap when interrelating different logical systems, particularly ones
that have not been as well defined rigorously, such as sequent calculus. Even as far as
semantics go on more formally defined logic such as classic propositional logic, concepts
like “completeness" and “soundness" between the “semantic" and the “deductive system"
is too arbitrarily defined …
Various Arithmetic Functions And Their Applications, Florentin Smarandache, Octavian Cira
Various Arithmetic Functions And Their Applications, Florentin Smarandache, Octavian Cira
Branch Mathematics and Statistics Faculty and Staff Publications
Over 300 sequences and many unsolved problems and conjectures related to them are presented herein. These notions, definitions, unsolved problems, questions, theorems corollaries, formulae, conjectures, examples, mathematical criteria, etc. on integer sequences, numbers, quotients, residues, exponents, sieves, pseudo-primes squares cubes factorials, almost primes, mobile periodicals, functions, tables, prime square factorial bases, generalized factorials, generalized palindromes, so on, have been extracted from the Archives of American Mathematics (University of Texas at Austin) and Arizona State University (Tempe): "The Florentin Smarandache papers" special collections, University of Craiova Library, and Arhivele Statului (Filiala Vâlcea & Filiala Dolj, România). The book is based on …
Neutrosophic Set Approach To Algebraic Structures, Florentin Smarandache, Madad Khan, Fazal Tahir
Neutrosophic Set Approach To Algebraic Structures, Florentin Smarandache, Madad Khan, Fazal Tahir
Branch Mathematics and Statistics Faculty and Staff Publications
Real world is featured with complex phenomenons. As uncertainty is inevitably involved in problems arise in various elds of life and classical methods failed to handle these type of problems. Dealing with imprecise, uncertain or imperfect information was a big task for many years. Many modelswerepresentedinordertoproperlyincorporateuncertaintyintosystem description, LotA.Zadeh in 1965 introduced the idea of a fuzzy set. Zadeh replaced conventional characteristic function of classical crisp sets which takes on its values in f0;1g by membership function which takes on its values in closed interval [0;1]. Fuzzy set theory is conceptually a very powerful technique to deal with another aspect or …
Strong Neutrosophic Graphs And Subgraph Topological Subspaces, Florentin Smarandache, W.B. Vasantha Kandasamy, Ilantheral K
Strong Neutrosophic Graphs And Subgraph Topological Subspaces, Florentin Smarandache, W.B. Vasantha Kandasamy, Ilantheral K
Branch Mathematics and Statistics Faculty and Staff Publications
In this book authors for the first time introduce the notion of strong neutrosophic graphs. They are very different from the usual graphs and neutrosophic graphs. Using these new structures special subgraph topological spaces are defined. Further special lattice graph of subgraphs of these graphs are defined and described. Several interesting properties using subgraphs of a strong neutrosophic graph are obtained. Several open conjectures are proposed. These new class of strong neutrosophic graphs will certainly find applications in NCMs, NRMs and NREs with appropriate modifications.
Interval-Valued Neutrosophic Oversets, Neutrosophic Undersets, And Neutrosophic Offsets, Florentin Smarandache
Interval-Valued Neutrosophic Oversets, Neutrosophic Undersets, And Neutrosophic Offsets, Florentin Smarandache
Branch Mathematics and Statistics Faculty and Staff Publications
We have proposed since 1995 the existence of degrees of membership of an element with respect to a neutrosophic set to also be partially or totally above 1 (over-membership), and partially or totally below 0 (under-membership) in order to better describe our world problems [published in 2007].
Neutrosophic Overset, Neutrosophic Underset, And Neutrosophic Offset. Similarly For Neutrosophic Over-/Under-/Off- Logic, Probability, And Statistics, Florentin Smarandache
Neutrosophic Overset, Neutrosophic Underset, And Neutrosophic Offset. Similarly For Neutrosophic Over-/Under-/Off- Logic, Probability, And Statistics, Florentin Smarandache
Branch Mathematics and Statistics Faculty and Staff Publications
Neutrosophic Over-/Under-/Off-Set and -Logic were defined for the first time by Smarandache in 1995 and published in 2007. They are totally different from other sets/logics/probabilities.
He extended the neutrosophic set respectively to Neutrosophic Overset {when some neutrosophic component is > 1}, Neutrosophic Underset {when some neutrosophic component is < 0}, and to Neutrosophic Offset {when some neutrosophic components are off the interval [0, 1], i.e. some neutrosophic component > 1 and other neutrosophic component < 0}.
This is no surprise with respect to the classical fuzzy set/logic, intuitionistic fuzzy set/logic, or classical/imprecise probability, where the values are not allowed outside the interval [0, 1], since our real-world has …
New Trends In Neutrosophic Theory And Applications - Vol. 1, Florentin Smarandache, Surapati Pramanik
New Trends In Neutrosophic Theory And Applications - Vol. 1, Florentin Smarandache, Surapati Pramanik
Branch Mathematics and Statistics Faculty and Staff Publications
Neutrosophic set has been derived from a new branch of philosophy, namely Neutrosophy. Neutrosophic set is capable of dealing with uncertainty, indeterminacy and inconsistent information. Neutrosophic set approaches are suitable to modeling problems with uncertainty, indeterminacy and inconsistent information in which human knowledge is necessary, and human evaluation is needed. Neutrosophic set theory was proposed in 1998 by Florentin Smarandache, who also developed the concept of single valued neutrosophic set, oriented towards real world scientific and engineering applications. Since then, the single valued neutrosophic set theory has been extensively studied in books and monographs introducing neutrosophic sets and its applications, …
Nidus Idearum. Scilogs, I: De Neutrosophia, Florentin Smarandache
Nidus Idearum. Scilogs, I: De Neutrosophia, Florentin Smarandache
Branch Mathematics and Statistics Faculty and Staff Publications
Welcome into my scientific lab! My lab[oratory] is a virtual facility with noncontrolled conditions in which I mostly perform scientific meditation and chats: a nest of ideas (nidus idearum, in Latin). I called the jottings herein scilogs (truncations of the words scientific, and gr. Λόγος – appealing rather to its original meanings "ground", "opinion", "expectation"), combining the welly of both science and informal (via internet) talks (in English, French, and Romanian). In this first books of scilogs collected from my nest of ideas, one may find new and old questions and solutions, some of them already put at work, others …
Nidus Idearum. Scilogs, Ii: De Rerum Consectatione, Florentin Smarandache
Nidus Idearum. Scilogs, Ii: De Rerum Consectatione, Florentin Smarandache
Branch Mathematics and Statistics Faculty and Staff Publications
Welcome into my scientific lab! My lab[oratory] is a virtual facility with noncontrolled conditions in which I mostly perform scientific meditation and chats: a nest of ideas (nidus idearum, in Latin). I called the jottings herein scilogs (truncations of the words scientific, and gr. Λόγος – appealing rather to its original meanings "ground", "opinion", "expectation"), combining the welly of both science and informal (via internet) talks (in English, French, and Romanian). In this second book of scilogs collected from my nest of ideas, one may find new and old questions and solutions, some of them already put at work, others …
Mathematics. Possible Subjects For The High School Entrance Examination And The Capacity Examination In Romania, Florentin Smarandache, Constantin Coanda, Ionuț Ivanescu
Mathematics. Possible Subjects For The High School Entrance Examination And The Capacity Examination In Romania, Florentin Smarandache, Constantin Coanda, Ionuț Ivanescu
Branch Mathematics and Statistics Faculty and Staff Publications
The present book tries to offer students and teachers knowledge evaluation tools for all the chapters from the current Romanian mathematics syllabus. In the evolution of teenagers, the phase of admission in high schools mobilizes particular efforts and emotions. The present workbook aims to be a permanent advisor in the agitated period starting with the capacity examination and leading to the admittance to high school. The tests included in this workbook have a complementary character as opposed to the many materials written with the purpose to support all those who prepare for such examinations and they refer to the entire …
Applying Dijkstra Algorithm For Solving Neutrosophic Shortest Path Problem, Florentin Smarandache, Luige Vladareanu, Said Broumi, Assia Bakali, Muhammad Akram
Applying Dijkstra Algorithm For Solving Neutrosophic Shortest Path Problem, Florentin Smarandache, Luige Vladareanu, Said Broumi, Assia Bakali, Muhammad Akram
Branch Mathematics and Statistics Faculty and Staff Publications
The selection of shortest path problem is one the classic problems in graph theory. In literature, many algorithms have been developed to provide a solution for shortest path problem in a network. One of common algorithms in solving shortest path problem is Dijkstra’s algorithm. In this paper, Dijkstra’s algorithm has been redesigned to handle the case in which most of parameters of a network are uncertain and given in terms of neutrosophic numbers. Finally, a numerical example is given to explain the proposed algorithm.
Pcr5 And Neutrosophic Probability In Target Identification, Florentin Smarandache, Nassim Abbas, Youcef Chibani, Bilal Hadjadji, Zayen Azzouz Omar
Pcr5 And Neutrosophic Probability In Target Identification, Florentin Smarandache, Nassim Abbas, Youcef Chibani, Bilal Hadjadji, Zayen Azzouz Omar
Branch Mathematics and Statistics Faculty and Staff Publications
In this paper we use PCR5 in order to fusion the information of two sources providing subjective probabilities of an event A to occur in the following form: chance that A occurs, indeterminate chance of occurrence of A, chance that A does not occur.
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, …