Sciweavers

CADE
2015
Springer
8 years 6 months ago
A Computational Logic Approach to Syllogisms in Human Reasoning
Psychological experiments on syllogistic reasoning have shown that participants did not always deduce the classical logically valid conclusions. In particular, the results show tha...
Emanuelle-Anna Dietz
CADE
2015
Springer
8 years 6 months ago
Inductive Beluga: Programming Proofs
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...
Brigitte Pientka, Andrew Cave
CADE
2015
Springer
8 years 6 months ago
Exploring Theories with a Model-Finding Assistant
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...
Salman Saghafi, Ryan Danas, Daniel J. Dougherty
CADE
2015
Springer
8 years 6 months ago
Encoding Dependency Pair Techniques and Control Strategies for Maximal Completion
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...
Haruhiko Sato, Sarah Winkler
CADE
2015
Springer
8 years 6 months ago
Beagle - A Hierarchic Superposition Theorem Prover
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...
Peter Baumgartner, Joshua Bax, Uwe Waldmann
CADE
2015
Springer
8 years 6 months ago
A Decision Procedure for (Co)datatypes in SMT Solvers
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...
Andrew Reynolds, Jasmin Christian Blanchette
CADE
2015
Springer
8 years 6 months ago
There is no one Logic to Model Human Reasoning: the Case from Interpretation
Alexandra Varga, Keith Stenning, Laura Martignon
CADE
2015
Springer
8 years 6 months ago
Termination Competition (termCOMP 2015)
Abstract. The termination competition focuses on automated termination analysis for all kinds of programming paradigms, including categories for term rewriting, imperative programm...
Jürgen Giesl, Frédéric Mesnard,...
CADE
2015
Springer
8 years 6 months ago
MathCheck: A Math Assistant via a Combination of Computer Algebra Systems and SAT Solvers
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
CADE
2015
Springer
8 years 6 months ago
A Formalisation of Finite Automata Using Hereditarily Finite Sets
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...
Lawrence C. Paulson