scientific article
From MaRDI portal
Publication:2751358
zbMath0992.03018MaRDI QIDQ2751358
Andreas Nonnengart, Christoph Weidenbach
Publication date: 27 August 2002
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
simplificationSkolemizationclause normal formCNF transformation of first-order predicate logic formulaeformula renaming
Related Items
A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic ⋮ Semantic forgetting in expressive description logics ⋮ Synthesis of positive logic programs for checking a class of definitions with infinite quantification ⋮ Second-Order Quantifier Elimination on Relational Monadic Formulas – A Basic Method and Some Less Expected Applications ⋮ Applying SAT solving in classification of finite algebras ⋮ Case splitting in an automatic theorem prover for real-valued special functions ⋮ HySAT: An efficient proof engine for bounded model checking of hybrid systems ⋮ Public announcements, public assignments and the complexity of their logic ⋮ Temporal Equilibrium Logic with past operators ⋮ Saturation-based Boolean conjunctive query answering and rewriting for the guarded quantification fragments ⋮ Superposition for higher-order logic ⋮ Coinductive models and normal forms for modal logics (or how we learned to stop worrying and love coinduction) ⋮ Automation for interactive proof: first prototype ⋮ Combining decision procedures by (model-)equality propagation ⋮ Deciding expressive description logics in the framework of resolution ⋮ Reasoning about norms under uncertainty in dynamic environments ⋮ Making theory reasoning simpler ⋮ Incremental search for conflict and unit instances of quantified formulas with E-matching ⋮ Reasoning in description logics by a reduction to disjunctive datalog ⋮ Pay-as-you-go consequence-based reasoning for the description logic \(\mathcal{SROIQ} \) ⋮ Theorem Proving in Large Formal Mathematics as an Emerging AI Field ⋮ Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs ⋮ Extended resolution simulates binary decision diagrams ⋮ An analog of the Cook theorem for polytopes ⋮ Translation of resolution proofs into short first-order proofs without choice axioms ⋮ Mechanising first-order temporal resolution ⋮ Resolution is cut-free ⋮ MPTP-motivation, implementation, first experiments ⋮ Extending Sledgehammer with SMT Solvers ⋮ Making higher-order superposition work ⋮ Making higher-order superposition work ⋮ Scalable fine-grained proofs for formula processing ⋮ Combining induction and saturation-based theorem proving ⋮ \(\mathrm{K}_{\mathrm S}\mathrm{P}\) a resolution-based theorem prover for \({\mathsf{K}}_n\): architecture, refinements, strategies and experiments ⋮ Effective Normalization Techniques for HOL ⋮ Predicate Elimination for Preprocessing in First-Order Theorem Proving ⋮ Superposition with first-class booleans and inprocessing clausification ⋮ Neural precedence recommender ⋮ SPASS-SATT. A CDCL(LA) solver ⋮ Induction in saturation-based proof search ⋮ Faster, higher, stronger: E 2.3 ⋮ Exploiting conjunctive queries in description logic programs ⋮ Labelled splitting ⋮ Semantic relevance ⋮ Extending Sledgehammer with SMT solvers ⋮ HermiT: an OWL 2 reasoner ⋮ SAT-Inspired Eliminations for Superposition
This page was built for publication:
