scientific article
From MaRDI portal
Publication:3150301
zbMath1020.68084MaRDI QIDQ3150301
Publication date: 30 September 2002
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Related Items
Deepalgebra -- an outline of a program, MaLeS: a framework for automatic tuning of automated theorem provers, MizAR 40 for Mizar 40, The higher-order prover \textsc{Leo}-II, Teaching Automated Theorem Proving by Example: PyRes 1.2, Implementing Superposition in iProver (System Description), ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description), Prolog Technology Reinforcement Learning Prover, From informal to formal proofs in Euclidean geometry, Portfolio theorem proving and prover runtime prediction for geometry, \textsf{lazyCoP}: lazy paramodulation meets neurally guided search, AC simplifications and closure redundancies in the superposition calculus, The role of entropy in guiding a connection prover, Learning theorem proving components, Quantifier-Free Equational Logic and Prime Implicate Generation, \( \alpha \)-paramodulation method for a lattice-valued logic \(L_nF(X)\) with equality, Things to know when implementing KBO, MizarMode -- an integrated proof assistance tool for the Mizar way of formalizing mathematics, \textit{Theorema}: Towards computer-aided mathematical theory exploration, The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0, MPTP 0.2: Design, implementation, and initial experiments, Extensional higher-order paramodulation in Leo-III, Unnamed Item, Blending under deconstruction. The roles of logic, ontology, and cognition in computational concept invention, Constraint solving for finite model finding in SMT solvers, The MET: The Art of Flexible Reasoning with Modalities, Machine Learning for Inductive Theorem Proving, CoProver: a recommender system for proof construction, Superposition for higher-order logic, Model evolution with equality -- revised and implemented, Efficient theory combination via Boolean search, Automated inference of finite unsatisfiability, Combining and automating classical and non-classical logics in classical higher-order logics, Automatic construction and verification of isotopy invariants, LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description), MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance, Engineering DPLL(T) + Saturation, Encapsulating formal methods within domain specific languages: a solution for verifying railway scheme plans, Learning-assisted theorem proving with millions of lemmas, Hammering Mizar by Learning Clause Guidance (Short Paper)., Using tableau to decide description logics with full role negation and identity, Harald Ganzinger’s Legacy: Contributions to Logics and Programming, Inst-Gen – A Modular Approach to Instantiation-Based Automated Reasoning, First-Order Resolution Methods for Modal Logics, Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs, Efficient instance retrieval with standard and relational path indexing, MPTP-motivation, implementation, first experiments, Sledgehammer: Judgement Day, Premise Selection in the Naproche System, On the Saturation of YAGO, HOL(y)Hammer: online ATP service for HOL Light, Automated Inference of Finite Unsatisfiability, TacticToe: learning to prove with tactics, Using First-Order Theorem Provers in the Jahob Data Structure Verification System, Finding Counter Examples in Induction Proofs, Superposition with lambdas, Making higher-order superposition work, Making higher-order superposition work, A comprehensive framework for saturation theorem proving, Extracting Higher-Order Goals from the Mizar Mathematical Library, Extending E Prover with Similarity Based Clause Selection Strategies, nanoCoP: A Non-clausal Connection Prover, Selecting the Selection, Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving, Superposition for full higher-order logic, Reliable reconstruction of fine-grained proofs in a proof assistant, The Isabelle/Naproche natural language proof assistant, Extending SMT solvers to higher-order logic, ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\), Old or heavy? Decaying gracefully with age/weight shapes, Induction in saturation-based proof search, Faster, higher, stronger: E 2.3, E Theorem Prover, Automated verification of refinement laws, A new methodology for developing deduction methods, A combinator-based superposition calculus for higher-order logic, A comprehensive framework for saturation theorem proving, Set of support, demodulation, paramodulation: a historical perspective, Bayesian ranking for strategy scheduling in automated theorem provers, Guiding an automated theorem prover with neural rewriting, Presenting and Explaining Mizar, An Interactive Derivation Viewer, The 10th IJCAR automated theorem proving system competition – CASC-J10, Distributing the Workload in a Lazy Theorem-Prover, SMELS: satisfiability modulo equality with lazy superposition, Machine learning for first-order theorem proving, Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\), Premise selection for mathematics by corpus analysis and kernel methods, SAT-Inspired Eliminations for Superposition, Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry
