14 citations · 17 across the 7 of their papers we have counts for
7 papers
Term Orders for Optimistic Lambda-Superposition
Alexander Bentkamp, Jasmin Blanchette, Matthias Hetzenberger
We introduce KBO and LPO, two variants of the Knuth-Bendix order (KBO) and the lexicographic path order (LPO) designed for use with the -superposition calculus. We establi…
Optimistic Higher-Order Superposition
Alexander Bentkamp, Jasmin Blanchette, Matthias Hetzenberger +1
The -superposition calculus is a successful approach to proving higher-order formulas. However, some parts of the calculus are extremely explosive, notably due to the higher-ord…
HHLPy: Practical Verification of Hybrid Systems using Hoare Logic
Huanhuan Sheng, Alexander Bentkamp, Bohua Zhan
We present a tool for verification of hybrid systems expressed in the sequential fragment of HCSP (Hybrid Communicating Sequential Processes). The tool permits annotating HCSP prog…
Privacy accounting conomics: Improving differential privacy composition via a posteriori bounds
Valentin Hartmann, Vincent Bindschaedler, Alexander Bentkamp +1
Differential privacy (DP) is a widely used notion for reasoning about privacy when publishing aggregate data. In this paper, we observe that certain DP mechanisms are amenable to a…
Superposition with Lambdas
Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret +2
We designed a superposition calculus for a clausal fragment of extensional polymorphic higher-order logic that includes anonymous functions but excludes Booleans. The inference rul…
Efficient Full Higher-Order Unification
Petar Vukmirović, Alexander Bentkamp, Visa Nummelin
We developed a procedure to enumerate complete sets of higher-order unifiers based on work by Jensen and Pietrzykowski. Our procedure removes many redundant unifiers by carefully r…
Superposition for Lambda-Free Higher-Order Logic
Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes +1
We introduce refutationally complete superposition calculi for intentional and extensional clausal -free higher-order logic, two formalisms that allow partial application and ap…