BibSLEIGH — Proceedings of the 21st International Conference on Automated Deduction

Frank Pfenning
Proceedings of the 21st International Conference on Automated Deduction
CADE, 2007.

TEST

@proceedings{CADE-2007,
	address       = "Bremen, Germany",
	editor        = "Frank Pfenning",
	isbn          = "978-3-540-73594-6",
	publisher     = "{Springer International Publishing}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 21st International Conference on Automated Deduction}",
	volume        = 4603,
	year          = 2007,
}

Contents (38 items)

CADE-2007-Stirling #automaton #game studies: Games, Automata and Matching (CS), pp. 1–2.
CADE-2007-HasanT #formal method #probability: Formalization of Continuous Probability Distributions (OH, ST), pp. 3–18.
CADE-2007-LiS #compilation #higher-order #logic: Compilation as Rewriting in Higher Order Logic (GL, KS), pp. 19–34.
CADE-2007-UrbanBN: Barendregt’s Variable Convention in Rule Inductions (CU, SB, MN), pp. 35–50.
CADE-2007-Harrison #automation #proving #using: Automating Elementary Number-Theoretic Proofs Using Gröbner Bases (JH), pp. 51–66.
CADE-2007-MotikSH #logic #reasoning #using: Optimized Reasoning in Description Logics Using Hypertableaux (BM, RS, IH), pp. 67–83.
CADE-2007-LutzW #lightweight #logic: Conservative Extensions in the Lightweight Description Logic EL (CL, FW), pp. 84–99.
CADE-2007-UnelT #incremental: An Incremental Technique for Automata-Based Decision Procedures (GÜ, DT), pp. 100–115.
CADE-2007-HeilalaP #bidirectional #logic: Bidirectional Decision Procedures for the Intuitionistic Propositional Modal Logic IS4 (SH, BP), pp. 116–131.
CADE-2007-AntonsenW: A Labelled System for IPL with Variable Splitting (RA, AW), pp. 132–146.
CADE-2007-TiwariG #logic #program analysis #proving #theorem proving #using: Logical Interpretation: Static Program Analysis Using Theorem Proving (AT, SG), pp. 147–166.
CADE-2007-GeBT #modulo theories #quantifier #satisfiability #using #verification: Solving Quantified Verification Conditions Using Satisfiability Modulo Theories (YG, CB, CT), pp. 167–182.
CADE-2007-MouraB #performance #smt: Efficient E-Matching for SMT Solvers (LMdM, NB), pp. 183–198.
CADE-2007-BonacinaE #composition: T-Decision by Decomposition (MPB, ME), pp. 199–214.
CADE-2007-KuncakR #algebra #performance #satisfiability #towards: Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic (VK, MCR), pp. 215–230.
CADE-2007-Aderhold: Improvements in Formula Generalization (MA), pp. 231–246.
CADE-2007-GodoyT #normalisation #on the #term rewriting: On the Normalization and Unique Normalization Properties of Term Rewrite Systems (GG, ST), pp. 247–262.
CADE-2007-CouchotL #automation #deduction #morphism #polymorphism: Handling Polymorphism in Automated Deduction (JFC, SL), pp. 263–278.
CADE-2007-HofnerS #algebra #automation #reasoning: Automated Reasoning in Kleene Algebra (PH, GS), pp. 279–294.
CADE-2007-SutcliffeP #axiom #named #semantics: SRASS — A Semantic Relevance Axiom Selection System (GS, YP), pp. 295–310.
CADE-2007-Lev-AmiWRS: Labelled Clauses (TLA, CW, TWR, MS), pp. 311–327.
CADE-2007-LynchT #automation #decidability #revisited: Automatic Decidability and Combinability Revisited (CL, DKT), pp. 328–344.
CADE-2007-Leino #design #verification: Designing Verification Conditions for Software (KRML), p. 345.
CADE-2007-PerezV #bound #effectiveness #encoding #logic #ltl #model checking: Encodings of Bounded LTL Model Checking in Effectively Propositional Logic (JANP, AV), pp. 346–361.
CADE-2007-GhilardiNRZ #infinity #model checking #satisfiability: Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems (SG, EN, SR, DZ), pp. 362–378.
CADE-2007-BeckertGHKRSS #component #deduction: The KeY system 1.0 (Deduction Component) (BB, MG, RH, VK, PR, SS, PHS), pp. 379–384.
CADE-2007-MurkLH #c #named #source code #verification: KeY-C: A Tool for Verification of C Programs (OM, DL, RH), pp. 385–390.
CADE-2007-BaeldeGMNT #model checking: The Bedwyr System for Model Checking over Syntactic Expressions (DB, AG, DM, GN, AT), pp. 391–397.
CADE-2007-VerchinineLP #automation #deduction #proving #verification: System for Automated Deduction (SAD): A Tool for Proof Verification (KV, AVL, AP), pp. 398–403.
CADE-2007-Baumgartner #logic: Logical Engineering with Instance-Based Methods (PB), pp. 404–409.
CADE-2007-KoprowskiM #dependence #predict #satisfiability #using: Predictive Labeling with Dependency Pairs Using SAT (AK, AM), pp. 410–425.
CADE-2007-FalkeK #dependence: Dependency Pairs for Rewriting with Non-free Constructors (SF, DK), pp. 426–442.
CADE-2007-GieslTSS #bound #proving #termination: Proving Termination by Bounded Increase (JG, RT, SS, PSK), pp. 443–459.
CADE-2007-Krauss #termination: Certified Size-Change Termination (AK), pp. 460–475.
CADE-2007-DeshaneHJLLM #encoding #first-order #proving #satisfiability: Encoding First Order Proofs in SAT (TD, WH, PJ, HL, CL, REM), pp. 476–491.
CADE-2007-BaumgartnerFP #similarity: Hyper Tableaux with Equality (PB, UF, BP), pp. 492–507.
CADE-2007-PelzerW: System Description: E-KRHyper (BP, CW), pp. 508–513.
CADE-2007-WeidenbachSHRT: System Description: SpassVersion 3.0 (CW, RAS, TH, RR, DT), pp. 514–520.

Frank PfenningProceedings of the 21st International Conference on Automated DeductionCADE, 2007.

Contents (38 items)

Frank Pfenning
Proceedings of the 21st International Conference on Automated Deduction
CADE, 2007.