You have Guest access.
Log In
Ulrich Furbach and Natarajan Shankar
Front matter
1-2
Mathematical Theory Exploration
3
Searching While Keeping a Trace: The Evolution from Satisfiability to Knowledge Compilation
4-20
Representing and Reasoning with Operational Semantics
21-35
Flyspeck I: Tame Graphs
36-51
Automatic Construction and Verification of Isotopy Invariants
52-66
Pitfalls of a Full Floating-Point Proof: Example on the Formal Proof of the Veltkamp/Dekker Algorithms
67-81
Using the TPTP Language for Writing Derivations and Finite Interpretations
82-96
Stratified Context Unification Is NP-Complete
97-111
A Logical Characterization of Forward and Backward Chaining in the Inverse Method
112-124
Connection Tableaux with Lazy Paramodulation
125-139
Blocking and Other Enhancements for Bottom-Up Model Generation Methods
140-144
The MathServe System for Semantic Web Reasoning Services
145-150
System Description: GCLCprover + GeoThms
151-155
A Sufficient Completeness Checker for Linear Order-Sorted Specifications Modulo Axioms
156-161
Extending the TPTP Language to Higher-Order Logic with Automated Parser Generation
162-176
Extracting Programs from Constructive HOL Proofs Via IZF Set-Theoretic Semantics
177-191
Towards Self-verification of HOL Light
192-204
An Interpretation of Isabelle/HOL in HOL Light
205-219
Combining Type Theory and Untyped Set Theory
220-234
Cut-Simulation in Impredicative Logics
235-250
Interpolation in Local Theory Extensions
251-265
Canonical Gentzen-Type Calculi with (n,k)-ary Quantifiers
266-280
Dynamic Logic with Non-rigid Functions A Basis for Object-Oriented Program Verification
281-286
AProVE 1.2: Automatic Termination Proofs in the Dependency Pair Framework
287-291
CEL — A Polynomial-Time Reasoner for Life Science Ontologies
292-297
FaCT++ Description Logic Reasoner: System Description
298-302
Importing HOL into Isabelle/HOL
303-317
Geometric Resolution: A Proof Procedure Based on Finite Model Search
318-331
A Powerful Technique to Eliminate Isomorphism in Finite Model Search
332-346
Automation of Recursive Path Ordering for Infinite Labelled Rewrite Systems
347-361
Strong Cut-Elimination Systems for Hudelmaier’s Depth-Bounded Sequent Calculus for Implicational Logic
362-376
Eliminating Redundancy in Higher-Order Unification: A Lightweight Approach
377-391
First-Order Logic with Dependent Types
392-407
Automating Proofs in Category Theory
408-422
Formal Global Optimisation with Taylor Models
423-437
A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers
438-452
Proving Formally the Implementation of an Efficient gcd Algorithm for Polynomials
453-467
A SAT-Based Decision Procedure for the Subclass of Unrollable List Formulas in ACL2 (SULFA)
468-482
Solving Sparse Linear Constraints
483-497
Inferring Network Invariants Automatically
498-512
A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL
513-527
Decidability and Undecidability Results for Nelson-Oppen and Rewrite-Based Decision Procedures
528-540
Verifying Mixed Real-Integer Quantifier Elimination
541-556
Presburger Modal Logic Is PSPACE-Complete
557-571
Tree Automata with Equality Constraints Modulo Equational Theories
572-573
CASC-J3 The 3rd IJCAR ATP System Competition
574-588
Matrix Interpretations for Proving Termination of Term Rewriting
589-603
Partial Recursive Functions in Higher-Order Logic
604-618
On the Strength of Proof-Irrelevant Type Theories
619-631
Consistency and Completeness of Rewriting in the Calculus of Constructions
632-646
Specifying and Reasoning About Dynamic Access-Control Policies
647-661
On Keys and Functional Dependencies as First-Class Citizens in Description Logics
662-677
A Resolution-Based Decision Procedure for SHOIQ\mathcal{SHOIQ}
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