Professional page of Simon Cruanes

NOTE: this page is old, see my personal page, which is more up-to-date.

I was a PhD student in the field of first-order automated deduction at Deducteam (INRIA) under the supervision of Gilles Dowek and Guillaume Burel. The subject I was working on is automated theorem proving modulo arithmetic and induction, and in general automated reasoning in the context of theories. I defended my thesis in September 2015.

Software

The following is all OCaml:

• Zipperposition, an experimental superposition prover
• Datalog, bottom-up and top-down datalog engines
• Logtk, a library for logic term and formula manipulation, used in Zipperposition
• Containers, an extension of OCaml's standard library

Teaching

My page about teaching (fr).

PhD Documents

• list of arithmetic files used for benchmarks (.tar.gz archive)
• Thesis, titled Extending Superposition with Integer Arithmetic, Structural Induction, and Beyond