Sciweavers

Beagle is an automated theorem prover for ﬁrst-order logic modulo built-in theories. It implements a reﬁned version of the hierarchic superposition calculus. This system descri...

Peter Baumgartner, Joshua Bax, Uwe Waldmann

claim paper

Read More »

188

Voted

CADE
2015
Springer

18views Logical Reasoning» more CADE 2015»

Encoding Dependency Pair Techniques and Control Strategies for Maximal Completion

9 years 10 months ago

Download kussharo.complex.ist.hokudai.ac.jp

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

claim paper

Read More »

187

Voted

CADE
2015
Springer

20views Logical Reasoning» more CADE 2015»

A Formalisation of Finite Automata Using Hereditarily Finite Sets

9 years 10 months ago

Download www.cl.cam.ac.uk

Abstract. Hereditarily ﬁnite (HF) set theory provides a standard universe of sets, but with no inﬁnite sets. Its utility is demonstrated through a formalisation of the theory o...

Lawrence C. Paulson

claim paper

Read More »

185

click to vote

CADE
2015
Springer

36views Logical Reasoning» more CADE 2015»

Inductive Beluga: Programming Proofs

9 years 10 months ago

Download www.cs.mcgill.ca

Abstract. beluga is a proof environment which provides a sophisticated infrastructure for implementing formal systems based on the logical framework LF together with a ﬁrst-order...

Brigitte Pientka, Andrew Cave

claim paper

Read More »

All Subjects

Algorithms

Applied Computing

Artificial Intelligence