You have Guest access.
Log In
Renate A. Schmidt
Front matter
1-16
Integrated Reasoning and Proof Choice Point Selection in the Jahob System – Mechanisms for Program Survival
17-34
Superposition and Model Evolution Combined
35-50
On Deciding Satisfiability by DPLL(G+T\Gamma+{\mathcal T}) and Unsound Theorem Proving
51-66
Combinable Extensions of Abelian Groups
67-83
Locality Results for Certain Extensions of Theories with Bridging Functions
84-99
Axiom Pinpointing in Lightweight Description Logics via Horn-SAT Encoding and Conflict Analysis
100-115
Does This Set of Clauses Overlap with at Least One MUS?
116-130
Progress in the Development of Automated Theorem Proving for Higher-Order Logic
131-139
System Description: H-PILoT
140-145
SPASS Version 3.5
146-150
Dei: A Theorem Prover for Terms with Integer Exponents
151-156
veriT: An Open, Trustable and Efficient SMT-Solver
157-162
Divvy: An ATP Meta-system Based on Axiom Relevance Ordering
163-166
Instantiation-Based Automated Reasoning: From Theory to Practice
167-182
Interpolant Generation for UTVPI
183-198
Ground Interpolation for Combined Theories
199-213
Interpolation and Symbol Elimination
214-229
Complexity and Algorithms for Monomial and Clausal Predicate Abstraction
230-244
Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method
245-260
A Refined Resolution Calculus for CTL
261-276
Fair Derivations in Monodic Temporal Reasoning
277-293
A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs
294-305
Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic
306-321
Building Theorem Provers
322-338
Termination Analysis by Dependency Pairs and Inductive Theorem Proving
339-354
Beyond Dependency Graphs
355-370
Computing Knowledge in Security Protocols under Convergent Equational Theories
371-387
Complexity of Fractran and Productivity
388-403
Automated Inference of Finite Unsatisfiability
404-420
Decidability Results for Saturation-Based Model Building
421-436
A Tableau Calculus for Regular Grammar Logics with Converse
437-452
An Optimal On-the-Fly Tableau-Based Decision Procedure for PDL-Satisfiability
453-468
Volume Computation for Boolean Combination of Linear Arithmetic Constraints
469-484
A Generalization of Semenov’s Theorem to Automata over Real Numbers
485-501
Real World Verification
Back matter
This page requires script.
Frequently asked questions General info on journals and books Send us your feedback Impressum Contact us
© Springer, Part of Springer Science+Business Media Privacy, Disclaimer, Terms & Conditions, and Copyright Info