scientific article; zbMATH DE number 2090305

zbMath1072.68596MaRDI QIDQ4809064

Christoph Weidenbach, Th. Hillenbrand, Dalibor Topić, Christian Theobald, Uwe Brahm, Enno Keen

Publication date: 12 August 2004

Full work available at URL: http://link.springer.de/link/service/series/0558/bibs/2392/23920275.htm

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

Mathematics Subject Classification ID

Related Items

The higher-order prover \textsc{Leo}-II, Assumption propagation through annotated programs, SAD as a mathematical assistant -- how should we go from here to there?, Crystal: Integrating structured queries into a tactic language, An Extension of the Knuth-Bendix Ordering with LPO-Like Properties, Automated inference of finite unsatisfiability, Automatic construction and verification of isotopy invariants, LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description), Engineering DPLL(T) + Saturation, Encapsulating formal methods within domain specific languages: a solution for verifying railway scheme plans, Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning, The Blossom of Finite Semantic Trees, From Search to Computation: Redundancy Criteria and Simplification at Work, First-Order Resolution Methods for Modal Logics, Statically safe program generation with SafeGen, Combining Top-Down and Bottom-Up Techniques in Program Derivation, SPASS, Presenting and Explaining Mizar, An Interactive Derivation Viewer