2 citations · 6 across the 4 of their papers we have counts for
4 papers
Translating Three-Variable First-Order Predicate Logic to Relation Algebra, Implemented using Z3
Anthony Brogni, Sebastiaan J. C. Joosten
This paper presents the development of a software tool that enables the translation of first-order predicate logic with at most three variables into relation algebra. The tool was…
Finding models through graph saturation
Sebastiaan J. C. Joosten
We give a procedure that can be used to automatically satisfy invariants of a certain shape. These invariants may be written with the operations intersection, composition and conve…
Initial Experiments with TPTP-style Automated Theorem Provers on ACL2 Problems
Sebastiaan Joosten, Cezary Kaliszyk, Josef Urban
This paper reports our initial experiments with using external ATP on some corpora built with the ACL2 system. This is intended to provide the first estimate about the usefulness o…
A Macro for Reusing Abstract Functions and Theorems
Sebastiaan J. C. Joosten, Bernard van Gastel, Julien Schmaltz
Even though the ACL2 logic is first order, the ACL2 system offers several mechanisms providing users with some operations akin to higher order logic ones. In this paper, we propose…