Result 1 to 20 of 24 total
More SPASS with Isabelle. Superposition with hard sorts and configurable simplification. (English)
Beringer, Lennart (ed.) et al., Interactive theorem proving. Third international conference, ITP 2012, Princeton, NJ, USA, August 13‒15, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-32346-1/pbk). Lecture Notes in Computer Science 7406, 345-360 (2012).
1
Monotonicity inference for higher-order formulas. (English)
J. Autom. Reasoning 47, No. 4, 369-398 (2011).
2
Automatic proof and disproof in Isabelle/HOL. (English)
Tinelli, Cesare (ed.) et al., Frontiers of combining systems. 8th international symposium, FroCoS 2011, Saarbrücken, Germany, October 5‒7, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-24363-9/pbk). Lecture Notes in Computer Science 6989. Lecture Notes in Artificial Intelligence, 12-27 (2011).
3
Extending Sledgehammer with SMT solvers. (English)
Bjørner, Nikolaj (ed.) et al., Automated deduction ‒ CADE-23. 23rd international conference on automated deduction, Wrocław, Poland, July 31 ‒ August 5, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-22437-9/pbk). Lecture Notes in Computer Science 6803. Lecture Notes in Artificial Intelligence, 116-130 (2011).
4
A material history of bits. (English)
J. Am. Soc. Inf. Sci. Technol. 62, No. 6, 1042-1057 (2011).
5
Extending sledgehammer with SMT solvers (English)
CADE, 116-130 (2011).
6
Automatic proof and disproof in isabelle/HOL (English)
FroCos, 12-27 (2011).
7
Nitpicking c++ concurrency (English)
PPDP, 113-124 (2011).
8
Generating counterexamples for structural inductions by exploiting nonstandard models. (English)
Fermüller, Christian G. (ed.) et al., Logic for programming, artificial intelligence, and reasoning. 17th international conference, LPAR-17, Yogyakarta, Indonesia, October 10‒15, 2010. Proceedings. Berlin: Springer (ISBN 978-3-642-16241-1/pbk). Lecture Notes in Computer Science 6397, 127-141 (2010).
9
Monotonicity inference for higher-order formulas. (English)
Giesl, Jürgen (ed.) et al., Automated reasoning. 5th international joint conference, IJCAR 2010, Edinburgh, UK, July 16‒19, 2010. Proceedings. Berlin: Springer (ISBN 978-3-642-14202-4/pbk). Lecture Notes in Computer Science 6173. Lecture Notes in Artificial Intelligence, 91-106 (2010).
10
Nitpick: A counterexample generator for higher-order logic based on a relational model finder. (English)
Kaufmann, Matt (ed.) et al., Interactive theorem proving. First international conference, ITP 2010, Edinburgh, UK, July 11‒14, 2010. Proceedings. Berlin: Springer (ISBN 978-3-642-14051-8/pbk). Lecture Notes in Computer Science 6172, 131-146 (2010).
11
Relational analysis of (co)inductive predicates, (co)algebraic datatypes, and (co)recursive functions. (English)
Fraser, Gordon (ed.) et al., Tests and proofs. 4th international conference, TAP 2010, Málaga, Spain, July 1‒2, 2010. Proceedings. Berlin: Springer (ISBN 978-3-642-13976-5/pbk). Lecture Notes in Computer Science 6143, 117-134 (2010).
12
Monotonicity inference for higher-order formulas (English)
IJCAR, 91-106 (2010).
13
Generating counterexamples for structural inductions by exploiting nonstandard models (English)
LPAR (Yogyakarta), 127-141 (2010).
14
Relational analysis of (Co)inductive predicates, (Co)algebraic datatypes, and (Co)recursive functions (English)
TAP, 117-134 (2010).
15
Nitpick: A counterexample generator for higher-order logic based on a relational model finder (English)
ITP, 131-146 (2010).
16
Intra-object versus inter-object: concurrency and reasoning in creol. (English)
Electron. Notes Theor. Comput. Sci. 243, 89-103 (2009).
17
Proof pearl: Mechanizing the textbook proof of Huffman’s algorithm. (English)
J. Autom. Reasoning 43, No. 1, 1-18 (2009).
18
An open system operational semantics for an object-oriented and component-based language. (English)
Electron. Notes Theor. Comput. Sci. 215, 151-169 (2008).
19
The digital signature dilemma (English)
Annales des Télécommunications 61, No. 7-8, 908-923 (2006).
20
Result 1 to 20 of 24 total
Start
Contact
Print
General Help
