CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Tip: Tools for inductive provers

Dan Rosén (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; Nicholas Smallbone (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers))
Lecture Notes in Computer Science. 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2015, Suva, Fiji, 24-28 November 2015 (0302-9743). Vol. 9450 (2015), p. 219-232.
[Konferensbidrag, refereegranskat]

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.

Denna post skapades 2016-01-18. Senast ändrad 2016-07-04.
CPL Pubid: 230830


Läs direkt!

Lokal fulltext (fritt tillgänglig)

Länk till annan sajt (kan kräva inloggning)

Institutioner (Chalmers)

Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)



Chalmers infrastruktur

Relaterade publikationer

Denna publikation ingår i:

Theory Exploration and Inductive Theorem Proving