BibTeX

@inProceedings{claessen-rosen-2015-modulo-230822,
	title        = {SAT modulo intuitionistic implications},
	abstract     = {We present a new method for solving problems in intuitionistic propositional logic, which involves the use of an incremental SAT-solver. The method scales to very large problems, and fits well into an SMT-based framework for interaction with other theories.},
	booktitle    = {Lecture Notes in Computer Science. Proceedings of the International Conferences on Logic for Programming, Artificial Intelligence and Reasoning (LPAR)},
	author       = {Claessen, Koen and Rosén, Dan},
	year         = {2015},
	volume       = {9450},
	ISBN         = {978-3-662-48898-0},
	pages        = {622--637},
}

@inProceedings{rosen-smallbone-2015-tools-230830,
	title        = {Tip: Tools for inductive provers},
	abstract     = {TIP is a toolbox for users and developers of inductive provers. It consists of a large number of tools which can, for example, simplify an inductive problem, monomorphise it or find counterexamples to it. We are using TIP to help maintain a set of benchmarks for inductive theorem provers, where its main job is to encode aspects of the problem that are not natively supported by the respective provers. TIP makes it easier to write inductive provers, by supplying necessary tools such as lemma discovery which prover authors can simply import into their own prover.},
	booktitle    = {Lecture Notes in Computer Science. 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2015, Suva, Fiji, 24-28 November 2015},
	author       = {Rosén, Dan and Smallbone, Nicholas},
	year         = {2015},
	volume       = {9450},
	ISBN         = {978-3-662-48898-0},
	pages        = {219--232},
}

@inProceedings{claessen-etal-2015-tons-222739,
	title        = {TIP: Tons of Inductive Problems},
	abstract     = {This paper describes our collection of benchmarks for inductive theorem provers. The recent spur of interest in automated inductive theorem proving has increased the demands for evaluation and comparison between systems. We expect the benchmark suite to continually grow as more problems are submitted by the community. New challenge problems will promote further development of provers which will greatly benefit both developers and users of inductive theorem provers.},
	booktitle    = {Lecture Notes in Artificial Intelligence: International Conference on Intelligent Computer Mathematics (CICM)},
	author       = {Claessen, Koen and Johansson, Moa and Rosén, Dan and Smallbone, Nicholas},
	year         = {2015},
	volume       = {9150},
	ISBN         = {978-3-319-20615-8},
	pages        = {332--336},
}