Easychair

swMATH13265MaRDI QIDQ25180FDOQ25180

Author name not available (Why is that?)

Cited In (49)

• Process algebra and model checking
• Uniform interpolation from cyclic proofs: the case of modal mu-calculus
• Scalable fine-grained proofs for formula processing
• Heterogeneous heuristic optimisation and scheduling for first-order theorem proving
• HR-SQL: extending SQL with hypothetical reasoning and improved recursion for current database systems
• Fast and slow enigmas and parental guidance
• Vampire with a brain is a good ITP hammer
• Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs
• The CADE-26 automated theorem proving system competition -- CASC-26
• Fuzzy intensional semantics
• Novel techniques to speed up the computation of the automorphism group of a graph
• On the decision problem for MELL
• Deciding Structural Liveness of Petri Nets
• Computer says no: verdict explainability for runtime monitors using a local proof system
• Counting with probabilistic and ultrametric finite automata
• Verification of Flat FIFO Systems
• Extensional higher-order paramodulation in Leo-III
• LPAR-21. 21st international conference on logic for programming, artificial intelligence and reasoning, Maun, Botswana, May 8--12, 2017. Selected papers
• Reducing complex CSP models to traces via priority
• Predicate Elimination for Preprocessing in First-Order Theorem Proving
• Performance of clause selection heuristics for saturation-based theorem proving
• Context-free commutative grammars with integer counters and resets
• Breaking symmetries in graph search with canonizing sets
• Layered clause selection for theory reasoning (short paper)
• Internal guidance for Satallax
• Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques
• Eliminating models during model elimination
• Learning theorem proving components
• Building strategies into QBF proofs
• ENIGMA: efficient learning-based inference guiding machine
• Complexity and resource bound analysis of imperative programs using difference constraints
• Set-theoretic analysis of nominative data
• The invariance problem for matrix semigroups
• Hierarchical invention of theorem proving strategies
• Inductive benchmarks for automated reasoning
• Craig interpolation with clausal first-order tableaux
• Covered clauses are not propagation redundant
• The CADE-28 Automated Theorem Proving System Competition – CASC-28
• Preprocessing for DQBF
• An Automation-Friendly Set Theory for the B Method
• \textsf{Goéland}: a concurrent tableau-based theorem prover (system description)
• Assigning papers to referees
• Linking focusing and resolution with selection
• Strong typed Böhm theorem and functional completeness on the linear lambda calculus
• Counterexample-Guided Model Synthesis
• Hammer for Coq: automation for dependent type theory
• A logic-based approach to incremental reasoning on multi-agent systems
• Efficient GPU algorithms for parallel decomposition of graphs into strongly connected and maximal end components
• Structural liveness of Petri nets is \textsc{ExpSpace}-hard and decidable

This page was built for software: Easychair