yusuke1997/dblp-id-title huggingface dataset:
An Experimental Evaluation of Global Caching for (System Description)
Tableaux Methods for Propositional Dynamic Logics with Separating Parallel Composition
On the Complexity of Fixed-Size Bit-Vector Logics with Binary Encoded Bit-Width
Names Are Not Just Sound and Smoke: Word Embeddings for Axiom Selection
A Sequent Calculus for First-Order Dynamic Logic with Trace Modalities
Problem Libraries for Non-Classical Logics
CSI: New Evidence - A Progress Report
IMPS: An Updated System Description
A Theory of Cartesian Arrays (with Applications in Quantum Circuit Verification)
ABSFOL: A Proof Checker with Abstraction
Automated Inference of Finite Unsatisfiability
Superposition for Divisible Torsion-Free Abelian Groups
A Breadth-First Strategy for Mating Search
STRIP: Structural Sharing for Efficient Proof-Search
Omega-MKRP: A Proof Development Environment
The Bedwyr System for Model Checking over Syntactic Expressions
Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings
Deductive Synthesis of Sorting Programs
Efficient SAT-based Proof Search in Intuitionistic Propositional Logic
Inducing Syntactic Cut-Elimination for Indexed Nested Sequents
Derived Preconditions and Their Use in Program Synthesis
A Comparative Study of Invariant Assertions, Invariant Relations, and Invariant Functions
Combining Proof-Search and Counter-Model Construction for Deciding Gödel-Dummett Logic
Uniform Substitution at One Fell Swoop
Designing Verification Conditions for Software
An Interval-based Temporal Logic in a Multivalued Setting
Efficient Algorithms for Computing Modulo Permutation Theories
Extending Decision Procedures with Induction Schemes
Introducing StarExec: a Cross-Community Infrastructure for Logic Solving
A Single-Significant-Digit Calculus for Semi-Automated Guesstimation
Termination Analysis by Inductive Evaluation
Admissibility of Fixpoint Induction over Partial Types
PRocH: Proof Reconstruction for HOL Light
System Description: Verification of Distributed Erlang Programs
The Romulus Proof Checker
Ontic: A Knowledge Representation System for Mathematics
Automated Deduction - CADE-19, 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28 - August 2, 2003, Proceedings
Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics
Automata Terms in a Lazy WSkS Decision Procedure
Towards Self-verification of HOL Light
DiaLog: A System for Dialogue Logic
Vampire Getting Noisy: Will Random Bits Help Conquer Chaos? (System Description)
There is no one Logic to Model Human Reasoning: the Case from Interpretation
Entailment vs. Verification for Partial-Assignment Satisfiability and Enumeration
Abstract Interpretation as Automated Deduction
Tutorial on Reasoning and Representation with Concept Languages
Proving Correctness of a KRK Chess Endgame Strategy by Using Isabelle/HOL and Z3
Towards SMT Model Checking of Array-Based Systems
Improved Modular Termination Proofs Using Dependency Pairs
Formal Verification of a Java Compiler in Isabelle
Some Notes on Basic Syntactic Mutation
Unbounded-Thread Program Verification using Thread-State Equations
The Impossibility of the Automation of Logical Reasoning
Abstract Domains for Bit-Level Machine Integer and Floating-point Operations
A High-Level Implementation of a System for Automated Reasoning with Default Rules (System Description)
Meta-Level Inference and Program Verification
Combinations of Theories and the Bernays-Schönfinkel-Ramsey Class
The Model Evolution Calculus with Equality
On Pot, Pans and Pudding or How to Discover Generalised Critical Pairs
A Mechanically Assisted Constructive Proof in Category Theory
Supposition-Based Logic for Automated Nonmontonic Reasoning
ACL2 Support for Verification Projects (Invited Talk)
N-PAT: A Nested Model-Checker - (System Description)
Reliable Reconstruction of Fine-grained Proofs in a Proof Assistant
Synthesising Functional Invariants in Separation Logic
Interoperability of Proof Systems with SC-TPTP
Relational Constraint Solving in SMT
Workshop: Type-Theoretic Languages: Proof-Search and Semantics
Proving Geometry Statements of Constructive Type
Mechanizable Inductive Proofs for a Class of Forall Exists Formulas
Termination Tools in Ordered Completion
Implicit Definitions with Differential Equations for KeYmaera X - (System Description)
Proof by Matrix Reduction as Plan + Validation
MetTeL 2 : Towards a Tableau Prover Generation Platform
Combining Multisets with Integers
Towards a Verified Tableau Prover for a Quantifier-Free Fragment of Set Theory
Proof Search and Proof Check for Equational and Inductive Theorems
Scrambling and Descrambling SMT-LIB Benchmarks
A Report in ICL HOL
VolCE: An Efficient Tool for Solving #SMT(LA) Problems
Rewriting Logic Semantics: From Language Specifications to Formal Analysis Tools
From Classical Extensional Higher-Order Tableau to Intuitionistic Intentional Natural Deduction
SPIKE: a System for Sufficient Completeness and Parameterized Inductive Proofs
System Description: Embedding Verification into Microsoft Excel
Unification in the Union of Disjoint Equational Theories: Combining Decision Procedures
Abstraction Mappings in Mechanical Theorem Proving
Tropical linear programming and parametric mean payoff games
The OWL Instance Store: System Description
Combination Techniques for Non-Disjoint Equational Theories
Approximating Dependency Graphs Using Tree Automata Techniques
Making Higher-Order Superposition Work
Automated Verification of Deontic Correspondences in Isabelle/HOL - First Results
MaLARea SG1- Machine Learner for Automated Reasoning with Semantic Guidance
Soft Subexponentials and Multiplexing
Actions over Core-Closed Knowledge Bases
A Complete Decision Procedure for Linearly Compositional Separation Logic with Data Constraints
Polynomial Interpretations and the Complexity of Algorithms
The Next Generation of Interactive Theorem Provers
Isabelle's Metalogic: Formalization and Proof Checker
PARTHENON: A Parallel Theorem Prover for Non-Horn Clauses
Some Contributions to the Logical Analysis of Circumscrition
Vampire@IJCAR 2016. Proceedings of the 3rd Vampire Workshop, Coimbra, Portugal, July 2, 2016
A Second-Order Theorem Prover Applied to Circumscription
System Description: lean K 2.0
Interactive Theorem Proving - Modelling the User in the Proof Process
The Logical Difference Problem for Description Logic Terminologies
The Char-Set Method and Its Applications to Automated Reasoning
EXPERT THINKER: An Adaptation of F-Prolog to Microcomputers
Automatic Theorem Proving in the ISDV System
Some Pitfalls of LK-to-LJ Translations and How to Avoid Them
Combining Deduction and Algebraic Constraints for Hybrid System Analysis
Inprocessing Rules
Making Automatic Theorem Provers more Versatile
Combining ProVerif and Automated Theorem Provers for Security Protocol Verification
Cyclic Proofs, Hypersequents, and Transitive Closure Logic
System Description: TRAMP: Transformation of Machine-Found Proofs into ND-Proofs at the Assertion Level
Diabelli: A Heterogeneous Proof System
Theory Links in Semantic Graphs
Proof Reuse for Program Verification Calculi
An Interactive Verification System Based on Dynamic Logic
Monotonicity Criteria for Polynomial Interpretations over the Naturals
Unification in a Combination of Equational Theories: an Efficient Algorithm
LIM+ Challenge Problems by RUE Hyper-Resolution
System Description: CutRes 0.1: Cut Elimination by Resolution
Short Proofs Without New Variables
Layered Clause Selection for Theory Reasoning - (Short Paper)
The Complexity of Finite Model Reasoning in Description Logics
Initial Experiments with External Provers and Premise Selection on HOL Light Corpora
EL -ifying Ontologies
Finding Good Proofs for Description Logic Entailments using Recursive Quality Measures
Computing Witnesses Using the SCAN Algorithm
On Incremental Pre-processing for SMT
Proving Termination by Bounded Increase
Theorem Proving with Group Presentations: Examples and Questions
A Certified Version of Buchberger's Algorithm
UNICOM: A Refined Completion Based Inductive Theorem Prover
&: Automated Natural Deduction
How QBF Expansion Makes Strategy Extraction Hard
Recursive Path Orderings Can Be Context-Sensitive
Sequent Calculi for Choice Logics
Optimizing Inconsistency-tolerant Description Logic Reasoning
Wellfounded Schematic Definitions
Introducing Quantified Cuts in Logic with Equality
Specification Inference and Invariant Generation: A Machine Learning Perspective
A New Clausal Class Decidable by Hyperresolution
Herod and Pilate: Two Tableau Provers for Basic Hybrid Logic
Single Axioms in the Implicational Propositional Calculus
Superposition with Datatypes and Codatatypes
m-NEVER System Summary
Tutorial on Program-Synthetic Deduction
An Improved General E-Unification Method
Automatic Proofs in Mathematical Logic and Analysis
Blocked Clause Elimination for QBF
Decision Procedures for Theories of Sets with Measures
MleanCoP: A Connection Prover for First-Order Modal Logic
Verifying Faradžev-Read Type Isomorph-Free Exhaustive Generation
Connection-Based Proof Construction in Linear Logic
A Goal Directed Theorem Prover
Towards Efficient "Knowledge-Based" Automated Theorem Proving for Non-Standard Logics
Analytic and Non-analytic Proofs
Dynamic Strategy Priority: Empower the Strong and Abandon the Weak
Dynamic Logic with Non-rigid Functions
Computing Transivity Tables: A Challenge For Automated Theorem Provers
Quantitative Separation Logic and Programs with Lists
A Framework for Verified Depth-First Algorithms
System Description: CRIL Platform for SAT
Analysis of Dependencies to Improve the Behaviour of Logic Programs
Race Against the Teens - Benchmarking Mechanized Math on Pre-university Problems
System Description: E.T. 0.1
Proceedings of the 5th Workshop on Practical Aspects of Automated Reasoning co-located with International Joint Conference on Automated Reasoning (IJCAR 2016), Coimbra, Portugal, July 2nd, 2016
Automated Reasoning in Kleene Algebra
The Aspect Calculus
EKL - A Mathematically Oriented Proof Checker
KPROP - An AND-parallel Theorem Prover for Propositional Logic implemented in KL1 (System Abstract)
STP: A Mechanized Logic for Specification and Verification
Complete Sets of Reductions with Constraints
Inferring Invariants by Symbolic Execution
System Abstract: E 0.61
Proving with BDDs and Control of Information
Subformula Linking for Intuitionistic Logic with Application to Type Theory
A Portable Environment for Research in Automated Reasoning
Simple Termination Revisited
The MathSAT 3 System
BDD-Based Decision Procedures for K
Benchmark Problems in Which Equality Plays the Major Role
10th International Conference on Automated Deduction, Kaiserslautern, FRG, July 24-27, 1990, Proceedings
A Programmer's Text Editor for a Logical Theory: The SUMOjEdit Editor (System Description)
Vampire 1.1 (System Description)
Challenges in Comparing Software Verification Tools for C
RegSTAB: A SAT Solver for Propositional Schemata
The GAZER Theorem Prover
An Overview of FRAPPS 2.0: A Framework for Resolution-based Automated Proof Procedure Systems
Transforming Termination by Self-Labelling
Logic & Proofs for Cyber-Physical Systems
Towards an Automatic Analysis of Security Protocols in First-Order Logic
Alternative Treatments of Common Binary Relations in First-order Automated Reasoning
Guiding Induction Proofs
CCE: Testing Ground Joinability
Perspectives on Automated Deduction (Abstract)
Lambda Logic
DCTP - A Disconnection Calculus Theorem Prover - System Abstract
Reduction and Unification in Lambda Calculi with Subtypes
Progress in Automating Higher-Order Ontology Reasoning
Tutorial on Rewrite-Based Theorem Proving
Decidability and Undecidability Results for Nelson-Oppen and Rewrite-Based Decision Procedures
A Machine-Checked Formalization of the Generic Model and the Random Oracle Model
GK: Implementing Full First Order Default Logic for Commonsense Reasoning (System Description)
Playing with AVATAR
Canonical Forms in Finitely Presented Algebras
PDL with Negation of Atomic Programs
Toward Mechanical Methods for Streamlining Proofs
Complexity Optimal Decision Procedure for a Propositional Dynamic Logic with Parallel Composition
Solving Difference Constraints over Modular Arithmetic
Efficient Instantiation Techniques in SMT (Work In Progress)
External Tools for the Formal Proof of the Kepler Conjecture
Model Finding for Recursive Functions in SMT
Semantic Entailment in Non Classical Logics Based on Proofs Found in Classical Logic
The Annual SUMO Reasoning Prizes at CASC
Computing Knowledge in Security Protocols under Convergent Equational Theories
A Why3 Framework for Reflection Proofs and Its Application to GMP's Algorithms
Abstract Congruence Closure and Specializations
SLIM: An Automated Reasoner For Equivalences, Applied To Set Theory
Challenges in the Automated Verification of Security Protocols
Mechanically Proving Geometry Theorems Using a Combination of Wu's Method and Collins' Method
Celf - A Logical Framework for Deductive and Concurrent Systems (System Description)
A Formally Verified, Optimized Monitor for Metric First-Order Dynamic Logic
Locality Results for Certain Extensions of Theories with Bridging Functions
A Logic for Verifying Metric Temporal Properties in Distributed Hybrid Systems
NIL: Learning Nonlinear Interpolants
Bottom-up Evaluation of Datalog Programs with Arithmetic Constraints
Satisfiability Checking and Query Answering for Large Ontologies
A Combination Method for Generating Interpolants
A Decision Procedure for (Co)datatypes in SMT Solvers
Choose Your Proofs: Commutativity and Symmetry for Smarter Reasoning
Decision Procedures for Some Fragments of Set Theory
Theorem Proving Systems of the Formel Project
Automated Reasoning - 6th International Joint Conference, IJCAR 2012, Manchester, UK, June 26-29, 2012. Proceedings
Representing and Reasoning with Operational Semantics
URBiVA: Uniform Reduction to Bit-Vector Arithmetic
Experiments in Automated Deduction with Condensed Detachment
Stochastic Differential Dynamic Logic for Stochastic Hybrid Programs
Proving Termination of Associative Commutative Rewriting Systems by Rewriting
Building Decision Procedures for Modal Logics from Propositional Decision Procedure - The Case Study of Modal K
A Comparison of Solvers for Propositional Dynamic Logic
Tableaux and Algorithms for Propositional Dynamic Logic with Converse
QBF Encoding of Temporal Properties and QBF-Based Verification
Superposition with First-class Booleans and Inprocessing Clausification
Basic Paramodulation and Superposition
Causes for Events: Their Computation and Applications
Rensets and Renaming-Based Recursion for Syntax with Bindings
On Keys and Functional Dependencies as First-Class Citizens in Description Logics
The HR Program for Theorem Generation
A Unifying Principle for Clause Elimination in First-Order Logic
Proof Assistants and the Dynamic Nature of Formal Theories
A Fast Verified Liveness Analysis in SSA Form
Term Ordering Diagrams
ZRES: The Old Davis-Putman Procedure Meets ZBDD
Automated Reasoning Contributed to Mathematics and Logic
Connecting Bits with Floating-Point Numbers: Model Checking and Theorem Proving in Practice
System Description: MathWeb, an Agent-Based Communication Layer for Distributed Automated Theorem Proving
Elements of Z-Module Reasoning
Non-well-founded Deduction for Induction and Coinduction
Buy One Get 14 Free: Evaluating Local Reductions for Modal Logic
Trends and Challenges in Satisfiability Modulo Theories
An Actual Implementation of a Procedure That Mechanically Proves Termination of Rewriting Systems Based on Inequalities Between Polynomial Interpretations
Twee: An Equational Theorem Prover
Selectively Instantiating Definitions
An nH-Prolog Implementation
A Simple Non-Termination Test for the Knuth-Bendix Method
An Algorithm for Deciding BAPA: Boolean Algebra with Presburger Arithmetic
Confluence by Critical Pair Analysis Revisited
A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT
Towards a Logic of Dilation
A Mechanizable Induction Principle for Equational Specifications
dTL2: Differential Temporal Dynamic Logic with Nested Temporalities for Hybrid Systems
On the Strength of Proof-Irrelevant Type Theories
Labelled Splitting
Blocking and Other Enhancements for Bottom-Up Model Generation Methods
Some Termination Criteria for Narrowing and E-Narrowing
Resource-Distribution via Boolean Constraint (Extended Abstract)
On Computational Models for Flash Memory Devices
Implementation of Approximation Algorithms for the Max-Min Resource Sharing Problem
A Nondifferentiable Optimization Approach to Ratio-Cut Partitioning
Experimental Comparison of Greedy Randomized Adaptive Search Procedures for the Maximum Diversity Problem
Computing the Exact Radius of Large Graphs
Noisy Sorting Without Searching: Data Oblivious Sorting with Comparison Errors
Parallel Flow-Based Hypergraph Partitioning
Experimental Algorithms, 9th International Symposium, SEA 2010, Ischia Island, Naples, Italy, May 20-22, 2010. Proceedings
Engineering Burstsort: Towards Fast In-Place String Sorting
Fast and Accurate Bounds on Linear Programs
Hierarchy Decomposition for Faster User Equilibria on Road Networks
Experimental and Efficient Algorithms, Third International Workshop, WEA 2004, Angra dos Reis, Brazil, May 25-28, 2004, Proceedings
Engineering Hybrid DenseZDDs
Dynamic Trees in Practice
Better Process Mapping and Sparse Quadratic Assignment
A New Relaxation for Tree-Based Problems and Minimum Power-Cost Spanning Trees
Empirical Analysis of the Connectivity Threshold of Mobile Agents on the Grid
A 3/2-Approximation Algorithm for the Student-Project Allocation Problem
Data Structures Resilient to Memory Faults: An Experimental Study of Dictionaries
Sparse Subgraphs for 2-Connectivity in Directed Graphs
On the Quadratic Shortest Path Problem
Improving Tree Search in Phylogenetic Reconstruction from Genome Rearrangement Data
Online Algorithm for Approximate Quantile Queries on Sliding Windows
A Clustering Algorithm for Interval Graph Test on Noisy Data
Relocation in Carsharing Systems Using Flows in Time-Expanded Networks
Experimental Studies of Graph Traversal Algorithms
Buffered Streaming Edge Partitioning
Relating Real and Synthetic Social Networks Through Centrality Measures
A Heuristic for Fair Correlation-Aware Resource Placement
Practical Compressed Suffix Trees
Energy Minimization via a Primal-Dual Algorithm for a Convex Program
A Practical Method for the Minimum Genus of a Graph: Models and Experiments
Automatic Decomposition and Branch-and-Price - A Status Report
Exact Graph Search Algorithms for Generalized Traveling Salesman Path Problems
DenseZDD: A Compact and Fast Index for Families of Sets
FREIGHT: Fast Streaming Hypergraph Partitioning
A Linear-Time Algorithm for Finding Induced Planar Subgraphs
A Framework for Designing Approximation Algorithms for Scheduling Problems
Approximating Interval Coloring and Max-Coloring in Chordal Graphs
On the Cost of Persistence and Authentication in Skip Lists
Fast and Simple Approximation of the Diameter and Radius of a Graph
Experimental Analysis of an Online Dictionary Matching Algorithm for Regular Expressions with Gaps
LCP Array Construction in External Memory
Finding Minimum Transmission Radii for Preserving Connectivity and Constructing Minimal Spanning Trees in Ad Hoc and Sensor Networks
Implementation of Approximation Algorithms for the Multicast Congestion Problem
Kernels for the Vertex Cover Problem on the Preferred Attachment Model
Separator Based Data Reduction for the Maximum Cut Problem
Practical Performance of Random Projections in Linear Programming
Characterizing the Performance of Flash Memory Storage Devices and Its Impact on Algorithm Design
The Hospitals / Residents Problem with Couples: Complexity and Integer Programming Models
Experimental Comparison of Semantic Word Clouds
An Experimental Evaluation of Semidefinite Programming and Spectral Algorithms for Max Cut
Polymorphic Cycle Basis in a Sequence of Graphs to Analyze the Structural Evolution of a Molecular Dynamic Trajectory
Engineering External Memory LCP Array Construction: Parallel, In-Place and Large Alphabet
Rotated-Box Trees: A Lightweight c-Oriented Bounding-Volume Hierarchy
From Theory to Practice: Plug and Play with Succinct Data Structures
Approximate Online Matching of Circular Strings
O'Reach: Even Faster Reachability in Large Graphs
Engineering Shared-Memory Parallel Shuffling to Generate Random Permutations In-Place
Experiments on Exact Crossing Minimization Using Column Generation
An Experimental Evaluation of Incremental and Hierarchical k -Median Algorithms
Competitive Buffer Management with Stochastic Packet Arrivals
A Multiple Sliding Windows Approach to Speed Up String Matching Algorithms
Localizing Program Logical Errors Using Extraction of Knowledge from Invariants
Fault Recovery in Wireless Networks: The Geometric Recolouring Approach
Integral Simplex Using Decomposition with Primal Cuts
Hierarchical Delaunay Triangulation for Meshing
22nd International Symposium on Experimental Algorithms, SEA 2024, Vienna, Austria, July 23-26, 2024
Convex Relaxation for the Generalized Maximum-Entropy Sampling Problem
Fast and Simple Compact Hashing via Bucketing
Evaluation of ILP-Based Approaches for Partitioning into Colorful Components
Parallelism in Current and Future Processors - Challenges and Support for Designing Optimal Algorithms
Experimental Evaluation of the Greedy and Random Algorithms for Finding Independent Sets in Random Graphs
A Branch-Price-and-Cut Algorithm for Packing Cuts in Undirected Graphs
Engineering A* Search for the Flip Distance of Plane Triangulations
Faster Compressed Suffix Trees for Repetitive Text Collections
20th International Symposium on Experimental Algorithms, SEA 2022, Heidelberg, Germany, July 25-27, 2022
Arc-Flags Meet Trip-Based Public Transit Routing
Practical Minimum Path Cover
19th International Symposium on Experimental Algorithms, SEA 2021, Nice, France, June 7-9, 2021
Rounding to an Integral Program
Frequency Assignment and Multicoloring Powers of Square and Triangular Meshes
Barcode Selection and Layout Optimization in Spatial Transcriptomics
Finding Connected Subgraphs of Fixed Minimum Density: Implementation and Experiments
Designing Energy-Efficient Heat Recovery Networks using Mixed-Integer Nonlinear Optimisation
Efficient Convergence to Pure Nash Equilibria in Weighted Network Congestion Games
In-Out Separation and Column Generation Stabilization by Dual Price Smoothing
Algorithms for Wireless Sensor Networks: Design, Analysis and Experimental Evaluation
Finding Modules in Networks with Non-modular Regions
Dominator Certification and Independent Spanning Trees: An Experimental Study
Using Bound Sets in Multiobjective Optimization: Application to the Biobjective Binary Knapsack Problem
Intriguingly Simple and Fast Transit Routing
A Hub-Based Labeling Algorithm for Shortest Paths in Road Networks
Efficient Route Planning with Temporary Driving Bans, Road Closures, and Rated Parking Areas
Concurrent Expandable AMQs on the Basis of Quotient Filters
Efficient Counting of Maximal Independent Sets in Sparse Graphs
Simple Max-Cut for Split-Indifference Graphs and Graphs with Few P 4 's
Efficient Computation of Jogging Routes
Solving and Generating Nagareru Puzzles
A Basic Toolbox for Constrained Quadratic 0/1 Optimization
Finding Hamiltonian Cycle in Graphs of Bounded Treewidth: Experimental Evaluation
Computing Vertex-Edge Cut-Pairs and 2-Edge Cuts in Practice
On Minimum Changeover Cost Arborescences
Practical Dynamic Entropy-Compressed Bitvectors with Applications
Relaxations of Multilinear Convex Envelopes: Dual Is Better Than Primal
Bulk-Insertion Sort: Towards Composite Measures of Presortedness
Beyond Unit Propagation in SAT Solving
Optimizing over the Efficient Set of a Multi-Objective Discrete Optimization Problem
A Framework of Dynamic Data Structures for String Processing
A Framework for Probabilistic Numerical Evaluation of Sensor Networks: A Case Study of a Localization Protocol
Greedy Heuristics for Judicious Hypergraph Partitioning
Automatic Tuning of GRASP with Path-Relinking Heuristics with a Biased Random-Key Genetic Algorithm
Memetic Graph Clustering