scientific article; zbMATH DE number 1765699

zbMath0988.03019MaRDI QIDQ4539640

Martin Giese

Publication date: 10 July 2002

Full work available at URL: http://link.springer.de/link/service/series/0558/bibs/2083/20830545

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

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items (13)

Theorem Proving with Bounded Rigid E-Unification ⋮ Proof generalization in \(\mathrm {LK}\) by second order unifier minimization ⋮ The model evolution calculus as a first-order DPLL method ⋮ Superposition-based equality handling for analytic tableaux ⋮ Liberalized variable splitting ⋮ Depth-first proof search without backtracking for free-variable clausal tableaux ⋮ Incremental variable splitting ⋮ First-order automated reasoning with theories: when deduction modulo theory meets practice ⋮ Towards a unified model of search in theorem-proving: subgoal-reduction strategies ⋮ KeY: A Formal Method for Object-Oriented Systems ⋮ Satisfiability Solving and Model Generation for Quantified First-Order Logic Formulas ⋮ Differential dynamic logic for hybrid systems ⋮ Solution lifting method for handling meta-variables in TH\(\exists\)OREM\(\forall\)

This page was built for publication: