scientific article
From MaRDI portal
Publication:2724150
zbMath0964.00020MaRDI QIDQ2724150
No author found.
Publication date: 9 July 2001
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Collections of articles of miscellaneous specific interest (00B15) Proceedings, conferences, collections, etc. pertaining to computer science (68-06) General reference works (handbooks, dictionaries, bibliographies, etc.) pertaining to computer science (68-00)
Related Items
Formal analysis of symbolic authenticity, Implementing Superposition in iProver (System Description), Alternating two-way AC-tree automata, The lengths of proofs: Kreisel's conjecture and Gödel's speed-up theorem, Towards finding longer proofs, History and Prospects for First-Order Automated Deduction, Optimal length resolution refutations of difference constraint systems, Proof planning with multiple strategies, Higher-order semantics and extensionality, Superposition-based equality handling for analytic tableaux, Normal forms for fuzzy logics: a proof-theoretic approach, On First-Order Model-Based Reasoning, An Impossible Asylum, Automating formalization by statistical and semantic parsing of mathematics, Proof systems for planning under 0-approximation semantics, Inference engine based on closure and join operators over truth table binary relations, A multi-clause dynamic deduction algorithm based on standard contradiction separation rule, The 11th IJCAR automated theorem proving system competition – CASC-J11, In Praise of Impredicativity: A Contribution to the Formalization of Meta-Programming, A formalisation of nominal \(\alpha\)-equivalence with A, C, and AC function symbols, Orienting rewrite rules with the Knuth-Bendix order., On structures of regular standard contradictions in propositional logic, Conjunctive Abstract Interpretation Using Paramodulation, Contradiction separation based dynamic multi-clause synergized automated deduction, Symbolic computation in automated program reasoning, Coinductive models and normal forms for modal logics (or how we learned to stop worrying and love coinduction), Resolution with order and selection for hybrid logics, NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment, Neural logic rule layers, Model evolution with equality -- revised and implemented, Automation for interactive proof: first prototype, Reliability of mathematical inference, Models and the dynamics of theory-building in physics. I: Modeling strategies, SMT proof checking using a logical framework, Reasoning processes in propositional logic, Unnamed Item, Efficient general AGH-unification, Glushkov's evidence algorithm, Reasoning on UML class diagrams, Counterexample-Guided Model Synthesis, Martin Davis’s Bibliography 1950–2015, Copy complexity of Horn formulas with respect to unit read-once resolution, Semantic classification of qualitative conditionals and calculating closures of nonmonotonic inference relations, Enhancing unsatisfiable cores for LTL with information on temporal relevance, On the mechanization of the proof of Hessenberg's theorem in coherent logic, The Blossom of Finite Semantic Trees, Rewriting Interpolants, The Logics' Explorer: a Maple package for exploring finite many-valued propositional logics, On the counting complexity of propositional circumscription, Reasoning about truth in first-order logic, How to Produce Information About a Given Entity Using Automated Deduction Methods, Abstraction and resolution modulo AC: How to verify Diffie--Hellman-like protocols automatically, Analogy in Automated Deduction: A Survey, Efficient instance retrieval with standard and relational path indexing, Loop invariants, Resolution is cut-free, Formal Verification of Graph Grammars using Mathematical Induction, Tractable query answering and rewriting under description logic constraints, A Decidable Class of Nested Iterated Schemata, Referential logic of proofs, Sequent forms of Herbrand theorem and their applications, Machine learning guidance for connection tableaux, Reasoning on Schemas of Formulas: An Automata-Based Approach, Lightweight relevance filtering for machine-generated resolution problems, Computing finite models by reduction to function-free clause logic, Shallow confluence of conditional term rewriting systems, Clausal presentation of theories in deduction modulo, MODULARITY IN MATHEMATICS, Normal forms of conditional knowledge bases respecting system P-entailments and signature renamings, First order Stålmarck. Universal lemmas through branch merges, Solving bitvectors with MCSAT: explanations from bits and pieces, Solution lifting method for handling meta-variables in TH\(\exists\)OREM\(\forall\), From Schütte’s Formal Systems to Modern Automated Deduction, A posthumous contribution by Larry Wos: excerpts from an unpublished column, Semantic relevance, Imperative LF Meta-Programming
