Updated research section on website

content/research/_index.md

@@ -5,6 +5,16 @@ Description: A list of my research Projects
 
 **[Quick List of Publications](publications)**
 
+**Research Interests:** Automated Reasoning, Artificial Intelligence, Formal Methods
+
+## Symbolic Methods for Cryptography
+Worked with Dr. Andrew Marshall under an ONR grant in collaboration with University at Albany, Clarkson University, University of Texas at Dallas, and the Naval Research lab in order to automatically generated and verify cryptographic algorithms using symbolic (as opposed to computational) methods.
+
+During that time period I built a free algebra library, rewrite library, parts of the crypto tool, and dabbled in Unification algorithms. You can check them out on [Github](https://github.com/symcollab/CryptoSolve).
+
+Currently, I am an external collaborator who mainly helps maintain the codebase I started as well as contribute to our current work with Garbled Circuits. We presented our work at [UNIF 2020](https://www3.risc.jku.at/publications/download/risc_6129/proceedings-UNIF2020.pdf#page=58) ([slides](/files/research/UNIF2020-Slides.pdf)), an accepted paper at FROCOS 2021, and have a couple other papers in the works.
+
+Through my collaborators, I've learned about term reasoning and algebras. [[Notes]](termreasoning)
 ## Reinforcement Learning
 
 **Deep Reinforcement Learning:** With Dr. Ron Zacharski I focused more on a particular instance of Reinforcement Learning where deep neural networks are used. During this time, I built out a Reinforcement Learning library written in PyTorch. This library helps me have a test bed for trying out different algorithms and attempts to create my own.
@@ -27,19 +37,13 @@ One particular problem I'm fascinated by is how to make Reinforcement Learning a
 [Github Code](https://github.com/brandon-rozek/ReinforcementLearning)
 
 
-## Symbolic Methods
-Worked with Dr. Andrew Marshall under an ONR grant in collaboration with University at Albany, Clarkson University, University of Texas at Dallas, and the Naval Research lab in order to automatically generated and verify cryptographic algorithms.
-
-During that time period I built a free algebra library, rewrite library, parts of the crypto tool, and dabbled in Unification algorithms. You can check them out on [Github](https://github.com/symcollab/CryptoSolve).
-
-Currently, I am an external collaborator who mainly helps maintain the codebase I started as well as contribute to our current work with Garbled Circuits. We presented our work at [UNIF 2020](https://www3.risc.jku.at/publications/download/risc_6129/proceedings-UNIF2020.pdf#page=58) ([slides](/files/research/UNIF2020-Slides.pdf)), an accepted paper at FROCOS 2021, and have a couple other papers in the works.
 
 
 ## Other
 
 **Programming Languages:** Studying the design of programming languages. So far I made an implementation of the SLOTH programming language, experimenting with what I want my own programming language to be syntatically and paradigm wise. [SLOTH Code](https://github.com/brandon-rozek/SLOTH)
 
-Before this study, I worked though a book called "Build your own Lisp" and my implementation of a lisp like language: [Lispy Code](https://github.com/brandon-rozek/lispy)
+Before this study, I worked though a book called ["Build your own Lisp"](https://www.buildyourownlisp.com/) and my implementation of a lisp like language: [Lispy Code](https://github.com/brandon-rozek/lispy)
 
 **Competitive Programming:** Studying algorithms and data structures necessary for competitive programming. Attended ACM ICPC in November 2018/2019 with a team of two other students.
 

content/research/publications.md

@@ -6,7 +6,7 @@ showthedate: false
 
 ## Papers
 
-(Accepted Paper TBA) Hai Lin, Christopher Lynch, Andrew M. Marshall, Catherine A. Meadows, Paliath Narendran, Veena Ravishankar, Brandon Rozek. "Algorithmic Problems in the Symbolic Approach to the Verification of Automatically Synthesized Cryptosystems", FROCOS, 2021.
+[Hai Lin, Christopher Lynch, Andrew M. Marshall, Catherine A. Meadows, Paliath Narendran, Veena Ravishankar, Brandon Rozek. "Algorithmic Problems in the Symbolic Approach to the Verification of Automatically Synthesized Cryptosystems", International Symposium on Frontiers of Combining Systems, 2021.](https://link.springer.com/chapter/10.1007/978-3-030-86205-3_14)
 
 
 ## Workshops

content/research/termreasoning.md

@@ -0,0 +1,58 @@
+---
+Title: Term Reasoning
+Description: Techniques that allow reasoning about term algebras.
+math: true
+---
+
+In this page, I wish to highlight techniques that are used to manipulate terms.
+
+## Unification
+Unification is a generalized form of equation solving taught in an algebra class. The goal is to find substitutions for variables such that the relation is true. 
+
+Example:
+$$
+f(a, x) = f(a, b)
+$$
+Result: $\sigma = \\{ x \mapsto b \\}$
+
+
+
+In the most general case, no theories or properties are assumed. Different unification algorithms are used based on the equational theory assumed. Most types of theories are denoted by a combination of letters:
+
+| Letter | Description           |
+| ------ | --------------------- |
+| A      | Associativity         |
+| C      | Commutativity         |
+| $D_l$  | Left Distributivity   |
+| $D_r$  | Right Distributivity  |
+| $I$    | Idempotence           |
+| $N_l$  | Left Neutral Element  |
+| $N_r$  | Right Neutral Element |
+
+The theory AC therefore has the associative and commutative property with respect to an operation. For a more complete reading on the subject, feel free to take a look at the Unification Theory chapter under "Handbook of Automated Reasoning, 2001".
+
+Additional Notes:
+- [Syntactic Unification](unification/syntactic)
+
+
+
+## Term Rewriting
+Term Rewriting is the study of replacing subterms of a formula. Normally they are described by a Rewrite Rule which in combination create a Rewrite System. 
+
+Example of a Rewrite Rule: $r_1 = f(a, x) \mapsto a$
+
+Example of a Rewrite System: $R = \\{r_0, r_2\\} = \\{ f(a, x) \mapsto a, f(x, b) \mapsto x \\}$
+
+Applying $r_1$ to $f(a, c)$ results in the term $c$. There are cases though when applying a rewrite rule to a term can create multiple results. This has to do with the subterm that is matched. For example, applying $r_1$ to $f(f(a, x), x)$ can result in either $f(a, x)$ or $a$ dependng on if you match the whole term or just the inner $f(a, x)$.
+
+The variants of a term is a set of terms reachable by applying a specified set of rewrite rules to the term. If the set of variants is finite for every term, then the Rewrite System is said to have the Finite Variant Property (FVP). 
+
+A great source for this topic is the book "Term Rewriting and All That" by Franz Baader and Tobias Nipkow.
+
+Additional Notes:
+- [Rewriting Algorithm](rewriting/algorithm)
+- [Variants Algorithm](rewriting/variants)
+- [Folding Variant Narrowing](rewriting/fv-narrowing)
+
+
+

content/research/termreasoning/rewriting/algorithm.md

@@ -0,0 +1,6 @@
+---
+title: Rewriting Algorithm
+math: true
+---
+
+This page is under construction...

content/research/termreasoning/rewriting/fv-narrowing.md

@@ -0,0 +1,6 @@
+---
+title: Folding Variant Narrowing
+math: true
+---
+
+This page is under construction...

content/research/termreasoning/rewriting/variants.md

@@ -0,0 +1,6 @@
+---
+title: Variants
+math: true
+---
+
+This page is under construction...

content/research/termreasoning/unification/syntactic.md

@@ -0,0 +1,37 @@
+---
+title: "Syntactic Unification"
+math: true
+---
+PAGE IS UNDER CONSTRUCTION...
+
+Unification is the more generalized form of equation solving that you might have learned in school. The goal is to find substitutions for variables to make the equality true. Syntactic unification is the simplest case, where we do not assume properties such as associativity, commutativity, distribution, etc. exist.
+
+In this post we're going to follow convention that constants are in the beginning half of the alphabet, while variables are in the later half.
+
+Constants: $a, b, c$
+
+Variables: $x, y, z$
+
+
+
+Algorithm:
+
+- Check for Occurs Check
+- Check for Function Clash
+- Orrient
+- Decompose
+
+
+
+Examples: (TODO: Walk through the algorithm)
+$$
+f(g(a, b)) =_? f(x)
+$$
+The solution to this problem is: $x \mapsto g(a, b)$ 
+
+
+$$
+f(g(a, b)) =_? x
+$$
+This has no solution.
+