The KeY system 1.0 (Deduction Component) (Englisch)
- Neue Suche nach: Beckert, Bernhard
- Neue Suche nach: Giese, Martin
- Neue Suche nach: Hähnle, Reiner
- Neue Suche nach: Klebanov, Vladimir
- Neue Suche nach: Rümmer, Philipp
- Neue Suche nach: Schlager, Steffen
- Neue Suche nach: Schmitt, Peter H.
- Neue Suche nach: Beckert, Bernhard
- Neue Suche nach: Giese, Martin
- Neue Suche nach: Hähnle, Reiner
- Neue Suche nach: Klebanov, Vladimir
- Neue Suche nach: Rümmer, Philipp
- Neue Suche nach: Schlager, Steffen
- Neue Suche nach: Schmitt, Peter H.
In:
Automated Deduction – CADE-21
10
;
379-384
;
2007
- Aufsatz/Kapitel (Buch) / Elektronische Ressource
-
Titel:The KeY system 1.0 (Deduction Component)
-
Beteiligte:Beckert, Bernhard ( Autor:in ) / Giese, Martin ( Autor:in ) / Hähnle, Reiner ( Autor:in ) / Klebanov, Vladimir ( Autor:in ) / Rümmer, Philipp ( Autor:in ) / Schlager, Steffen ( Autor:in ) / Schmitt, Peter H. ( Autor:in )
-
Erschienen in:Automated Deduction – CADE-21 , 10 ; 379-384Lecture Notes in Computer Science ; 4603, 10 ; 379-384
-
Verlag:
- Neue Suche nach: Springer Berlin Heidelberg
-
Erscheinungsort:Berlin, Heidelberg
-
Erscheinungsdatum:01.01.2007
-
Format / Umfang:6 pages
-
ISBN:
-
ISSN:
-
DOI:
-
Medientyp:Aufsatz/Kapitel (Buch)
-
Format:Elektronische Ressource
-
Sprache:Englisch
-
Schlagwörter:
-
Datenquelle:
Inhaltsverzeichnis E-Book
Die Inhaltsverzeichnisse werden automatisch erzeugt und basieren auf den im Index des TIB-Portals verfügbaren Einzelnachweisen der enthaltenen Beiträge. Die Anzeige der Inhaltsverzeichnisse kann daher unvollständig oder lückenhaft sein.
- 1
-
Games, Automata and MatchingStirling, Colin et al. | 2007
- 3
-
Formalization of Continuous Probability DistributionsHasan, Osman / Tahar, Sofiène et al. | 2007
- 19
-
Compilation as Rewriting in Higher Order LogicLi, Guodong / Slind, Konrad et al. | 2007
- 35
-
Barendregt’s Variable Convention in Rule InductionsUrban, Christian / Berghofer, Stefan / Norrish, Michael et al. | 2007
- 51
-
Automating Elementary Number-Theoretic Proofs Using Gröbner BasesHarrison, John et al. | 2007
- 67
-
Optimized Reasoning in Description Logics Using HypertableauxMotik, Boris / Shearer, Rob / Horrocks, Ian et al. | 2007
- 84
-
Conservative Extensions in the Lightweight Description Logic $\mathcal{EL}$Lutz, Carsten / Wolterinst, Frank et al. | 2007
- 100
-
An Incremental Technique for Automata-Based Decision ProceduresUnel, Gulay / Toman, David et al. | 2007
- 116
-
Bidirectional Decision Procedures for the Intuitionistic Propositional Modal Logic IS4Heilala, Samuli / Pientka, Brigitte et al. | 2007
- 132
-
A Labelled System for IPL with Variable SplittingAntonsen, Roger / Waaler, Arild et al. | 2007
- 147
-
Logical Interpretation: Static Program Analysis Using Theorem ProvingTiwari, Ashish / Gulwani, Sumit et al. | 2007
- 167
-
Solving Quantified Verification Conditions Using Satisfiability Modulo TheoriesGe, Yeting / Barrett, Clark / Tinelli, Cesare et al. | 2007
- 183
-
Efficient E-Matching for SMT SolversMoura, Leonardo / Bjørner, Nikolaj et al. | 2007
- 199
-
${\mathcal{T}}$ -Decision by DecompositionBonacina, Maria Paola / Echenim, Mnacho et al. | 2007
- 215
-
Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger ArithmeticKuncak, Viktor / Rinard, Martin et al. | 2007
- 231
-
Improvements in Formula GeneralizationAderhold, Markus et al. | 2007
- 247
-
On the Normalization and Unique Normalization Properties of Term Rewrite SystemsGodoy, Guillem / Tison, Sophie et al. | 2007
- 263
-
Handling Polymorphism in Automated DeductionCouchot, Jean-François / Lescuyer, Stéphane et al. | 2007
- 279
-
Automated Reasoning in Kleene AlgebraHöfner, Peter / Struth, Georg et al. | 2007
- 295
-
SRASS - A Semantic Relevance Axiom Selection SystemSutcliffe, Geoff / Puzis, Yury et al. | 2007
- 311
-
Labelled ClausesLev-Ami, Tal / Weidenbach, Christoph / Reps, Thomas / Sagiv, Mooly et al. | 2007
- 328
-
Automatic Decidability and Combinability RevisitedLynch, Christopher / Tran, Duc-Khanh et al. | 2007
- 345
-
Designing Verification Conditions for SoftwareLeino, K. Rustan M. et al. | 2007
- 346
-
Encodings of Bounded LTL Model Checking in Effectively Propositional LogicNavarro-Pérez, Juan Antonio / Voronkov, Andrei et al. | 2007
- 362
-
Combination Methods for Satisfiability and Model-Checking of Infinite-State SystemsGhilardi, Silvio / Nicolini, Enrica / Ranise, Silvio / Zucchelli, Daniele et al. | 2007
- 379
-
The KeY system 1.0 (Deduction Component)Beckert, Bernhard / Giese, Martin / Hähnle, Reiner / Klebanov, Vladimir / Rümmer, Philipp / Schlager, Steffen / Schmitt, Peter H. et al. | 2007
- 385
-
KeY-C: A Tool for Verification of C ProgramsMürk, Oleg / Larsson, Daniel / Hähnle, Reiner et al. | 2007
- 391
-
The Bedwyr System for Model Checking over Syntactic ExpressionsBaelde, David / Gacek, Andrew / Miller, Dale / Nadathur, Gopalan / Tiu, Alwen et al. | 2007
- 398
-
System for Automated Deduction (SAD): A Tool for Proof VerificationVerchinine, Konstantin / Lyaletski, Alexander / Paskevich, Andrei et al. | 2007
- 404
-
Logical Engineering with Instance-Based MethodsBaumgartner, Peter et al. | 2007
- 410
-
Predictive Labeling with Dependency Pairs Using SATKoprowski, Adam / Middeldorp, Aart et al. | 2007
- 426
-
Dependency Pairs for Rewriting with Non-free ConstructorsFalke, Stephan / Kapur, Deepak et al. | 2007
- 443
-
Proving Termination by Bounded IncreaseGiesl, Jürgen / Thiemann, René / Swiderski, Stephan / Schneider-Kamp, Peter et al. | 2007
- 460
-
Certified Size-Change TerminationKrauss, Alexander et al. | 2007
- 476
-
Encoding First Order Proofs in SATDeshane, Todd / Hu, Wenjin / Jablonski, Patty / Lin, Hai / Lynch, Christopher / McGregor, Ralph Eric et al. | 2007
- 492
-
Hyper Tableaux with EqualityBaumgartner, Peter / Furbach, Ulrich / Pelzer, Björn et al. | 2007
- 508
-
System Description: E- KRHyperPelzer, Björn / Wernhard, Christoph et al. | 2007
- 514
-
System Description: Spass Version 3.0Weidenbach, Christoph / Schmidt, Renate A. / Hillenbrand, Thomas / Rusev, Rostislav / Topic, Dalibor et al. | 2007