98 citations · 647 across the 44 of their papers we have counts for
3 papers · 2 filters
A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL
Katherine Kosaian, Yong Kiam Tan, André Platzer
We formalize a multivariate quantifier elimination (QE) algorithm in the theorem prover Isabelle/HOL. Our algorithm is complete, in that it is able to reduce any quantified formula…
Implicit Definitions with Differential Equations for KeYmaera X (System Description)
James Gallicchio, Yong Kiam Tan, Stefan Mitsch +1
Definition packages in theorem provers provide users with means of defining and organizing concepts of interest. This system description presents a new definition package for the h…
First-Order Game Logic and Modal Mu-Calculus
Noah Abou El Wafa, André Platzer
This paper investigates first-order game logic and first-order modal mu-calculus, which extend their propositional modal logic counterparts with first-order modalities of interpret…