Updates to research page

content/research/_index.md

@@ -7,66 +7,65 @@ Description: A list of my research Projects
 
 **Broad Research Interests:** Automated Reasoning, Automated Planning, Artificial Intelligence, Formal Methods
 
-Currently, I'm a Computer Science PhD Candidate at Rensselaer Polytechnic Institute. I enjoy using logic-based techniques and designing algorithms to solve problems.
+I'm a Computer Science PhD Candidate at Rensselaer Polytechnic Institute. I enjoy using logic-based techniques and designing algorithms to solve problems.
 
 Jump to:
-- [Planning under uncertainty](#planning-under-uncertainty)
-- [Logic](#logic)
-- [Symbolic Methods for Cryptography](#symbolic-methods-for-cryptography)
+- [Automated Planning under uncertainty](#automated-planning-under-uncertainty)
+- [Computational and Formal Logic](#computational-and-formal-logic)
+- [Verifying Cryptographic Properties](#verifying-cryptographic-properties)
 
-## Planning under Uncertainty
+## Automated Planning under Uncertainty
 
-My dissertation topic is on automatically finding and recognizing plans
-when agents are uncertain about the environment but can compare the
-uncertainty between events *qualitatively*. For example, it is totally
+My dissertation topic is on designing algorithms to automatically find
+and recognize plans when agents are uncertain about their environment
+but can compare the uncertainty between events *qualitatively*.
+
+For example, it is totally
 expected when we stack a block that it stays on the top. However, there is a
 smaller likelihood that the block falls off.
-How can we best make use of this qualitative uncertainty?
-- Agents when operating under uncertainty will seek plans which maximize the likelihood of their goals.
+How can we best make use of this information?
+- When recognizing the goals of agents, one assumption we can make is that the agent is
+following a plan that maximizes the likelihood of reaching their goals.
 I designed an algorithm for recognizing these plans under qualitative possibility theory. This work is supervised under [Selmer Bringsjord](https://kryten.mm.rpi.edu/selmerbringsjord.html) (Paper to be released soon)
-- Additionally with Selmer Bringsjord in the [RAIR Lab](https://rair.cogsci.rpi.edu/), I created a framework that captures
-situations where agents are able to bucket the likelihood of facts within their environment. I then provide an effective
-techinque for using classical planners to find plans which maximize the agent's likelihood of success. ([Paper](/paper/2406.02))
+- Additionally with Selmer Bringsjord in the [RAIR Lab](https://rair.cogsci.rpi.edu/), I created a framework for when agents are able to bucket the likelihood of facts within their environment. I then provide an effective
+technique for using classical planners to find a plan which maximizes the agent's likelihood of success. ([Paper](/paper/2406.02))
 - In the RAIR Lab, I also further developed [Spectra](https://github.com/rairlab/spectra) --
 an automated planner built on automated theorem proving. I showed how a class of problems
-under uncertainty can be easily encoded and wrote a question-answer algorithm
+under uncertainty can be easily encoded, and I implemented a question-answer algorithm
 for ShadowProver so that Spectra can find plans under epistemic uncertainty. ([Paper](/paper/2405.01/))
 - With [Junkyu Lee](https://researcher.ibm.com/researcher/view.php?person=ibm-Junkyu.Lee),
 [Michael Katz](https://researcher.watson.ibm.com/researcher/view.php?person=ibm-Michael.Katz1),
 [Harsha Kokel](https://harshakokel.com/), and [Shirin Sohrabi](https://researcher.watson.ibm.com/researcher/view.php?person=us-ssohrab) at IBM I developed an algorithm
 for guiding hierarchical reinforcement agents under partial observability. Specifically,
-I focused on situations where the agent knows what they don't know and compiled that knowledge
-so that a fully-observable non-deterministic planner can decompose the overall problem. ([Paper](/paper/2406.01))
+I focused on scenarios where the agent knows what they don't know, and I compiled that knowledge
+to use a fully-observable non-deterministic planner to decompose the overall problem. ([Paper](/paper/2406.01))
 
-## Logic
+## Computational and Formal Logic
 
-Underlying my work in artificial intelligence and cryptography
-is computational logic. In that regard, I have been able
-work on problems from the underlying logic formalisms,
-unification algorithms, to building
-tools for interactive theorem provers.
-
-- With [Andrew Tedder](https://sites.google.com/view/andrewjtedder/research), I'm currently working
-on building a tool that checks if matrix models of given logic satisfies relevance properties.
-- With [Andrew Marshall](https://www.marshallandrew.net/) and [Kimberly Cornell](https://www.albany.edu/cehc/faculty/kimberly-cornell), we're currently developing a new syntactic AC algorithm.
-- With [Thomas Ferguson](https://faculty.rpi.edu/thomas-ferguson) and [James Oswald](https://jamesoswald.dev) we formalized a model theory for a fragment of the Deontic Cognitive Event Calculus.
-- With James Oswald we've built interactive theorem provers and showed validity of large proofs in parallel using a high performance cluster.
+I have a deep fascination of using logic as a tool to model problems. In that regard, I have been fortunate to work with some excellent collaborators on designing logic formalisms, studying properties of logic systems,
+and implementing solvers and verifiers.
+- With [Andrew Tedder](https://sites.google.com/view/andrewjtedder/research), we built a tool
+which can efficiently determine in polynomial time (for a class of logics) whether a matrix model satisfies
+the variable sharing property. This property is frequently studied in the relevance logic literature and is often a starting point for other stronger properties. (Paper to be released soon)
+- With [Andrew Wells](https://andrewmw94.github.io/) at Amazon Web Services, I built a tool which takes in a supported
+fragment of TypeScript, and uses the Dafny verification language to determine whether two functions are equivalent. I wrote the compiler using the Lean 4 programming language, and included several dataflow analysis passes to capture whether the function may have exited at a certain program point, raised an exception, etc.
+- With [Andrew Marshall](https://www.marshallandrew.net/) and [Kimberly Cornell](https://www.albany.edu/cehc/faculty/kimberly-cornell), we dedicated effort to designing a new AC unification algorithm that works directly on formulae instead
+of compiling to a diophantine solver. This project is currently on hold.
+- With [Thomas Ferguson](https://faculty.rpi.edu/thomas-ferguson) and [James Oswald](https://jamesoswald.dev), we formalized a model theory for a fragment of the Deontic Cognitive Event Calculus. ([Paper](/paper/2405.02))
+- With James Oswald, we've built an interactive theorem prover ([Project](https://github.com/RAIRLab/lazyslate)) and showed validity of large proofs in parallel using a high performance cluster. ([Paper](/paper/2311.01/))
 
 
 Related Notes:
 
 - [Automated Theorem Proving](atp/)
 - [Term Reasoning](termreasoning/)
- 
 
-## Symbolic Methods for Cryptography
-Worked with [Andrew Marshall](https://www.marshallandrew.net/) and others in applying term reasoning within computational logic
-towards cryptography. This collaboration was previously funded under an ONR grant. We are interested in applying techniques such
-as unification and term rewriting to the following areas:
-- Block Ciphers
-- Secure Multi-party Computation
-- Authentication
-- Commitment Schemes
+
+## Verifying Cryptographic Properties
+Worked with [Andrew Marshall](https://www.marshallandrew.net/) and others in designing and implementing
+unification algorithms for verifying cryptographic properties. Our team looked at block ciphers, multi-party computation,
+authentication, and commitment schemes. During my time working with this team, I focused on verifying whether
+block ciphers are protected against the indistinguishability under chosen plaintext attack.
 
 Together we built [CryptoSolve](https://github.com/cryptosolvers/CryptoSolve), a symbolic cryptographic analysis tool, and made it publically available on GitHub. I wrote the term algebra and rewrite libraries, and contributed to the mode of operation library and some unification algorithms.
 I still help maintain the codebase. We previously presented our work