This site uses cookies to deliver our services and to ensure you get the best experience. By continuing to use this site, you consent to our use of cookies and acknowledge that you have read and understand our Privacy Policy, Cookie Policy, and Terms
Psychological experiments on syllogistic reasoning have shown that participants did not always deduce the classical logically valid conclusions. In particular, the results show tha...
Abstract. beluga is a proof environment which provides a sophisticated infrastructure for implementing formal systems based on the logical framework LF together with a first-order...
We present an approach to understanding first-order theories by exploring their models. A typical use case is the analysis of artifacts such as policies, protocols, configuration...
Abstract. This paper describes two advancements of SAT-based KnuthBendix completion as implemented in Maxcomp. (1) Termination techniques using the dependency pair framework are en...
Beagle is an automated theorem prover for first-order logic modulo built-in theories. It implements a refined version of the hierarchic superposition calculus. This system descri...
Abstract. We present a decision procedure that combines reasoning about datatypes and codatatypes. The dual of the acyclicity rule for datatypes is a uniqueness rule that identifi...
Abstract. The termination competition focuses on automated termination analysis for all kinds of programming paradigms, including categories for term rewriting, imperative programm...
Abstract. We present a method and an associated system, called MathCheck, that embeds the functionality of a computer algebra system (CAS) within the inner loop of a conflict-driv...
Edward Zulkoski, Vijay Ganesh, Krzysztof Czarnecki
Abstract. Hereditarily finite (HF) set theory provides a standard universe of sets, but with no infinite sets. Its utility is demonstrated through a formalisation of the theory o...