yusuke1997/dblp-id-title huggingface dataset:
A Semantics for a Class of Non-Deterministic and Causal Production System Programs
On Protocols for the Automated Discovery of Theorems in Elementary Geometry
HermiT: An OWL 2 Reasoner
Invariant-Free Clausal Temporal Resolution
Analyzing Program Termination and Complexity Automatically with AProVE
Completeness Issues in RUE-NRF Deduction: The Undecidability of Viability
Logic, Topology, and Integration
On Fourier's Algorithm for Linear Arithmetic Constraints
Formal Reasoning Under Cached Address Translation
Implementing the 'Fool's Model' of Combinatory Logic
The Locally Nameless Representation
Decidability Issues for Extended Ping-Pong Protocols
Current Trends in Logical Frameworks and Metalanguages
Special Issue of Selected Extended Papers of IJCAR 2020
Unification Modulo ACUI Plus Distributivity Axioms
What Holds in a Context?
The Automation of Syllogistic
A New Reduction Rule for the Connection Graph Proof Procedure
The CADE-18 ATP System Competition
Automatically Proving Termination and Memory Safety for Programs with Pointer Arithmetic
An O(nlog n)-SPACE Decision Procedure for the Propositional Dummett Logic
Interactive Theorem Proving - Preface of the Special Issue
Resolution with Order and Selection for Hybrid Logics
Theory Extension in ACL2(r)
The Warshall Algorithm and Dickson's Lemma: Two Examples of Realistic Program Extraction
Formalising Szemerédi's Regularity Lemma and Roth's Theorem on Arithmetic Progressions in Isabelle/HOL
Horn Equational Theories and Paramodulation
Craig Interpolation with Clausal First-Order Tableaux
Encoding Abstract Syntax Without Fresh Names
Parallel Postulates and Continuity Axioms: A Mechanized Study in Intuitionistic Logic Using Coq
Set-Var
Tool-Assisted Specification and Verification of Typed Low-Level Languages
The Right Tools for the Job: Correctness of Cone of Influence Reduction Proved Using ACL2 and HOL4
Decidability and Combination Results for Two Notions of Knowledge in Security Protocols
A Mechanized Proof of the Max-Flow Min-Cut Theorem for Countable Networks with Applications to Probability Theory
Strategies for Modal Resolution: Results and Problems
Larry Wos: Visions of Automated Reasoning
A Path Ordering for Proving Termination of AC Rewrite Systems
Comparing Parameter Schemes for Propositional Reasoning: An Empirical Study
Regular Random k -SAT: Properties of Balanced Formulas
The Reflective Milawa Theorem Prover is Sound (Down to the Machine Code that Runs it)
Finite-valued Semantics for Canonical Labelled Calculi
Completeness and Decidability Results for CTL in Constructive Type Theory
Solving Non-Boolean Satisfiability Problems with Stochastic Local Search: A Comparison of Encodings
A Tableau-Based Decision Procedure for a Fragment of Set Theory with Iterated Membership
An Improved Refutation System for Intuitionistic Predicate Logic
Geometry Constructions Language
Preface: Special Issue on Interpolation
Interest Driven Suppositional Reasoning
Higher-Order Quantifier Elimination, Counter Simulations and Fault-Tolerant Systems
Schubert's Steamroller Problem: Formulation and Solutions
Six Decades of Automated Reasoning: Papers in Memory of Larry Wos
A Canonical Locally Named Representation of Binding
Preface: Special Issue of Selected Extended Papers of CADE-22
A Framework for Proof Systems
Verifying Whiley Programs with Boogie
TacticToe: Learning to Prove with Tactics
Interprocedural and Flow-Sensitive Type Analysis for Memory and Type Safety of C Code
Approaching Hard Non-Classical Problems
Testing Positiveness of Polynomials
Correction to: Differential Dynamic Logic for Hybrid Systems
Computer Proofs in Group Theory
Efficient Strategies for CEGAR-Based Model Checking
An Extensible Encoding of Object-oriented Data Models in hol
The Problem of Choosing the Representation, Inference Rule, and Strategy
Derivational Complexity and Context-Sensitive Rewriting
Single Axioms for Odd Exponent Groups
Incremental Classification of Description Logics Ontologies
ExpTime Tableaux for ALC Using Sound Global Caching
Gale-Shapley Verified
The Problem of Reasoning from Inequalities
Reconsidering Pairs and Functions as Sets
Preface: Special Issue on Automatic Resource Bound Analysis
Termination of String Rewriting Proved Automatically
An Inexact Reasoning Algorithm Based on Fuzzy Rule Matrix Transformations
Linear Depth Deduction with Subformula Property for Intuitionistic Epistemic Logic
A Proof Procedure for the Logic of Hereditary Harrop Formulas
Automating Boolean Set Operations in Mizar Proof Checking with the Aid of an External SAT Solver
Automated Generation of Readable Proofs with Geometric Invariants
A Direct Procedure to Test Entailment in a Separation Logic of Relations
Automated Discovery of New Axiomatizations of the Left Group and Right Group Calculi
A Logic Programming System for Nonmonotonic Reasoning
Answer Set Programming Based on Propositional Satisfiability
Explaining Gabriel-Zisman Localization to the Computer
Nonconstructive Computational Mathematics
Single Versus Simultaneous Equational Unification and Equational Unification for Variable-Permuting Theories
Mechanical Verification of an Ideal Incremental ABR Conformance Algorithm
Toupie: The µ-calculus over Finite Domains as a Constraint Language
Mark Stickel: His Earliest Work
Verification of FPGA Layout Generators in Higher-Order Logic
Multi-cost Bounded Tradeoff Analysis in MDP
Semantic Generalizations for Proving and Disproving Conjectures by Analogy
Automated Proofs of Equality Problems in Overbeek's Competition
Guided Local Search for Solving SAT and Weighted MAX-SAT Problems
Analogy in Inductive Theorem Proving
Verifying Programs with Logic and Extended Proof Rules: Deep Embedding vs. Shallow Embedding
A Mechanised Proof of Gödel's Incompleteness Theorems Using Nominal Isabelle
Positive Unit Hyperresolution Tableaux and Their Application to Minimal Model Generation
An Automatically Verified Prototype of the Tokeneer ID Station Specification
Optimizing Terminological Reasoning for Expressive Description Logics
A Simple and Efficient Boolean Solver for Constraint Logic Programming
First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems: Automation, Formalization, Certification
Adding Decision Procedures to SMT Solvers Using Axioms with Triggers
A lambda-Unifiability Test for Set Theory
MPTP - Motivation, Implementation, First Experiments
Proving Termination by Dependency Pairs and Inductive Theorem Proving
The Tail-Recursive SECD Machine
Formal Correctness of a Quadratic Unification Algorithm
A Calculus for and Termination of Rippling
VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs
Combining Higher-Order Logic with Set Theory Formalizations
A Bi-Directional Extensible Interface Between Lean and Mathematica
Non-Linear Rewrite Closure and Weak Normalization
Proving Matijasevich's Lemma with a Default Arithmetic Strategy
Locales: A Module System for Mathematical Theories
Elimination of Self-Resolving Clauses
A Solution to the PoplMark Challenge Based on de Bruijn Indices
Using Bounded Model Checking for Coverage Analysis of Safety-Critical Software in an Industrial Setting
Linear Numeral Systems
Custom Automations in Mizar
Producing Proofs of Unsatisfiability with Distributed Clause-Sharing SAT Solvers
RRTP - A Replacement Rule Theorem Prover
Fermat, Euler, Wilson - Three Case Studies in Number Theory
First -Order Syntactic Characterizations of Minimal Entailment, Domain-Minimal Entailment, and Herbrand Entailment
Equivalence of Propositional Prolog Programs
A Wos Challenge Met
Natural Projection as Partial Model Checking
Choices in Representation and Reduction Strategies for Lambda Terms in Intensional Contexts
Programming in Temporal-Nonmonotonic Reasoning
Automatic Synthesis of Logical Models for Order-Sorted First-Order Theories
Certifying Low-Level Programs with Hardware Interrupts and Preemptive Threads
Optimal Length Resolution Refutations of Difference Constraint Systems
Top-Down Query Processing in First-Order Deductive Databases under the DWFS
Bisequent Calculus for Four-Valued Quasi-Relevant Logics: Cut Elimination and Interpolation
SATCHMORE: SATCHMO with REIevancy
On the Importance of Domain Model Configuration for Automated Planning Engines
Parallelization of a Hyper-Linking-Based Theorem Prover
Automated Reducible Geometric Theorem Proving and Discovery by Gröbner Basis Method
A Foray Into Combinatory Logic
Mechanically Proving Termination Using Polynomial Interpretations
Unification Algorithms for Eliminating and Introducing Quantifiers in Natural Deduction Automated Theorem Proving
Protected Completions of First-Order General Logic Programs
Formalizing Synthetic Domain Theory
Verifying Safety and Persistence in Hybrid Systems Using Flowpipes and Continuous Invariants
On Deciding Satisfiability by Theorem Proving with Speculative Inferences
Refinement to Imperative HOL
A Skeptic's Approach to Combining HOL and Maple
Resolution is Cut-Free
A SAT Solver Using Reconfigurable Hardware and Virtual Logic
The Problem of Reasoning by Case Analysis
Structures for Abstract Rewriting
Automated Reasoning with Power Maps
How to Clear a Block: A Theory of Plans
Differential Dynamic Logic for Hybrid Systems
Declarative Representation of Proof Terms
Mechanical Verification of Strategies
Single Axioms for Groups
TABLEAUX: A General Theorem Prover for Modal Logics
Experiments with Proof Plans for Induction
Finitary Type Theories With and Without Contexts
A Tableau Algorithm for Description Logics with Concrete Domains and General TBoxes
Generating Relevant Models
Preface: Special Issue of Selected Extended Papers of CADE-23
Verifying the SET Purchase Protocols
Fast Subsumption Checks Using Anti-Links
Automatic Refinement to Efficient Data Structures: A Comparison of Two Approaches
Knowledge Compilation Using the Extension Rule
Resolution Theorem Proving in Reified Modal Logics
Formalizing Adequacy: A Case Study for Higher-order Abstract Syntax
LINUS - A Link Instantion Prover with Unit Support
Decidability by Resolution for Propositional Modal Logics
Formalization and Implementation of Modern SAT Solvers
Computer-Assisted Proofs for Lyapunov Stability via Sums of Squares Certificates and Constructive Analysis
Kit and the Short Stack
Conflict Resolution: A First-Order Resolution Calculus with Decision Literals and Conflict-Driven Clause Learning
Seventy-Five Problems for Testing Automatic Theorem Provers
Correctness Criteria of Some Algorithms for Uncertain Reasoning Using Incidence Calculus
An Erratum for Some Errata to ATP Problems
Special Issue on Security and Rewriting Foreword
Semantically-Guided Goal-Sensitive Reasoning: Inference System and Completeness
Formalized Functional Analysis with Semilinear Maps
KBO Orientability
Towards a Scalable Proof Engine: A Performant Prototype Rewriting Primitive for Coq
Modality and Interrupts
Efficient Active Automata Learning via Mutation Testing
Tractable Extensions of the Description Logic ${\mathcal{EL}}$ with Numerical Datatypes
Self-Formalisation of Higher-Order Logic - Semantics, Soundness, and a Verified Implementation
An Experiment with the Boyer-Moore Theorem Prover: A Proof of Wilson's Theorem
Fast Term Indexing with Coded Context Trees
Fast, Verified Computation for HOL ITPs
Deciding Boolean Algebra with Presburger Arithmetic
Experimenting with Isabelle in ZF Set Theory
Vanquishing the XCB Question: The Methodological Discovery of the Last Shortest Single Axiom for the Equivalential Calculus
Liberalized Variable Splitting
Automated Production of Traditional Proofs in Solid Geometry
Erratum to: Conflict Resolution: A First-Order Resolution Calculus with Decision Literals and Conflict-Driven Clause Learning
Fast Formal Proof of the Erdős-Szekeres Conjecture for Convex Polygons with at Most 6 Points
Proving Fairness and Implementation Correctness of a Microkernel Scheduler
An Automatically Verified Prototype of the Android Permissions System
Selected Extended Papers of NFM 2016: Preface
Characterizations of the Disjunctive Well-Founded Semantics: Confluent Calculi and Iterated GCWA
Tilting at Windmills with Coq: Formal Verification of a Compilation Algorithm for Parallel Moves
SPS-Parallelism + SETHEO = SPTHEO
An Automata-Theoretic Approach to Model-Checking Systems and Specifications Over Infinite Data Domains
Designing Deductive Databases
Gentzen-Type Systems, Resolution and Tableaux
Solution Validation and Extraction for QBF Preprocessing
Proof Tree Preserving Tree Interpolation
The Liberalized delta-Rule in Free Variable Semantic Tableaux
A Trustworthy Proof Checker
A Model-Based Belief Revision System
Proving Equivalence of Different Axiomatizations of Free Groups
Proving Unsatisfiability of CNFs Locally
Proof Reflection in Coq
Linear and Unit-Resulting Refutations for Horn Theories
Verifying Termination and Reduction Properties about Higher-Order Logic Programs
Deduction in Non-Horn Databases
A Learning-Based Approach to Synthesizing Invariants for Incomplete Verification Engines
Automated Reasoning about Elementary Point-Set Topology
Axiomatizing the Skew Boolean Propositional Calculus
SAT Meets Tableaux for Linear Temporal Logic Satisfiability
What You Always Wanted to Know about Rigid E-Unification
Automated Development of Tarski's Geometry
CLIN-E - Smallest Instance First Hyper-Linking
A More Expressive Formulation of Many Sorted Logic
Tractable Reasoning and Efficient Query Answering in Description Logics: The DL-Lite Family
Constructing the Lie Algebra of Smooth Vector Fields on a Lie Group in Isabelle/HOL
Inference Rules Using Local Contexts
I-SATCHMO: An Improvement of SATCHMO
Single-Set Cubical Categories and Their Formalisation with a Proof Assistant
From Signatures to Monads in UniMath
The Problem of Reasoning by Analogy
Herbrand Award Acceptance Speech
Computing Only Minimal Answers in Disjunctive Deductive Databases
Automatic Symmetry Detection for Promela
MPTP 0.2: Design, Implementation, and Initial Experiments
Mathematical Programming Embeddings of Logic
Decision Procedures for the Security of Protocols with Probabilistic Encryption against Offline Dictionary Attacks
Evaluating Optimized Decision Procedures for Propositional Modal K(m) Satisfiability
Recognizing Unnecessary Clauses in Resolution Based Systems
Otter - The CADE-13 Competition Incarnations
Preface: Special Issue on Homotopy Type Theory and Univalent Foundations
From Specification to Testing: Semantics Engineering for Lua 5.2
Theorem Proving Modulo
The Flow of ODEs: Formalization of Variational Equation and Poincaré Map
A Method for the Mechanical Derivation of Formulas in Elementary Geometry
Algorithms and Proofs Inheritancey in the FOC Language
Combining SAT Solvers with Computer Algebra Systems to Verify Combinatorial Conjectures
Finite Reasons for Safety - Parameterized Verification by Finite Model Finding
The Kernel Strategy and Its Use for the Study of Combinatory Logic
A Formalisation in HOL of the Fundamental Theorem of Linear Algebra and Its Application to the Solution of the Least Squares Problem
Combining Sets with Cardinals
Decidable ∃ *∀ * First-Order Fragments of Linear Rational Arithmetic with Uninterpreted Predicates
The TPTP Problem Library and Associated Infrastructure - From CNF to TH0, TPTP v6.4.0
Ordinal Arithmetic: Algorithms and Mechanization
A Class of Confluent Term Rewriting Systems and Unification
On Equivalents of Well-Foundedness
Well-Behaved Inference Rules for First-Order Theorem Proving
The CADE-15 ATP System Competition
A Formalization of the CHSH Inequality and Tsirelson's Upper-bound in Isabelle/HOL
Managing Structural Information by Higher-Order Colored Unification
Condensed Detachment is Complete for Relevance Logic: A Computer-Aided Proof
Type-Based Cost Analysis for Lazy Functional Languages
Soundness and Completeness Proofs by Coinductive Methods
Reachability Analysis over Term Rewriting Systems
Abductive Theorem Proving for Analyzing Student Explanations to Guide Feedback in Intelligent Tutoring Systems
Computer Assisted Reasoning
Informational Logic as a Tool for Automated Reasoning
Near-Horn Prolog and Beyond
The Problem of Choosing between Using and Avoiding Eqyality Predicates
The Problem of Naming and Function Replacement
Set Theory for Verification: I. From Foundations to Functions
Implementing Tactics and Tacticals in a Higher-Order Logic Programming Language
Visually Dynamic Presentation of Proofs in Plane Geometry - Part 1. Basic Features and the Manual Input Method
Structure Sharing for Quantified Terms: Fundamentals
Automated Proofs of Löb's Theorem and Gödel's Two Incompleteness Theorems
SETHEO: A High-Performance Theorem Prover
SAT Local Search Algorithms: Worst-Case Study
Autoepistemic Logic of First Order and Its Expressive Power
Algorithms for Finding Matrix Models of Propositional Calculi
On the Termination of Clause Graph Resolution
Verifying the Correctness and Amortized Complexity of a Union-Find Implementation in Separation Logic with Time Credits
A Comparison of the Variable-Abstraction and Constant-Abstraction Methods for Associative-Commutative Unification
Cutting to the Chase - Solving Linear Integer Arithmetic
Inferring Phylogenetic Trees Using Answer Set Programming
Loop-Type Sequent Calculi for Temporal Logic
Automated Generation of Geometry Proof Problems Based on Point Geometry Identity
A Combined Superposition and Model Evolution Calculus
Experiments with Discrimination-Tree Indexing and Path Indexing for Term Retrieval
First-order Hybrid Separation Logic
Checking Simple Properties of Transition Systems Defined by Thue Specifications
Contraction-Free Linear Depth Sequent Calculi for Intuitionistic Propositional Logic with the Subformula Property and Minimal Depth Counter-Models
Verifying OpenJDK's Sort Method for Generic Collections
Pattern-Directed Invocation with Changing Equations
The Saturated Tableaux for Linear Miniscoped Horn-like Temporal Logic
A Mechanical Proof of Quadratic Reciprocity
Mechanising Gödel-Löb Provability Logic in HOL Light
Combining Stable Infiniteness and (Strong) Politeness
6 Years of SMT-COMP
Many-Sorted Equivalence of Shiny and Strongly Polite Theories
Searching for Shortest Single Axioms for Groups of Exponent 6
Heavy-Tailed Phenomena in Satisfiability and Constraint Satisfaction Problems
Computing Knowledge in Security Protocols Under Convergent Equational Theories
Productive Use of Failure in Inductive Proof
On Automation in the Verification of Software Barriers: Experience Report
Machine Learning Guidance for Connection Tableaux
Formally Verified Certificate Checkers for Hardest-to-Round Computation
A Correct Logic Programming Computation of Default Logic Extensions
Java Bytecode Verification
Translation of IEC 61131-3 Function Block Diagrams to PVS for Formal Verification with Real-Time Nuclear Application
Single Axioms for Groups and Abelian Groups with Various Operations
Satisfiability Checking in Łukasiewicz Logic as Finite Constraint Satisfaction
The Power of Combining Resonance with Heat
Non-Horn Clause Logic Programming Without Contrapositives
The TPTP Problem Library and Associated Infrastructure
The James Construction and π 4 (S 3 ) in Homotopy Type Theory
A Completion Procedure for Finitely Presented Groups That Is Based on Word Cycles
Multi-Attacker Protocol Validation
Elimination Transformations for Associative-Commutative Rewriting Systems
Formal Analysis of Multiparty Contract Signing
A Proof Environment for Teaching Mathematics
Attacking Group Protocols by Refuting Incorrect Inductive Conjectures
Definitional Expansions in Mizar - In memoriam of Andrzej Trybulec, a pioneer of computerized formalization
SPTHEO - A Parallel Theorem Prover
Linear Resources in Isabelle/HOL
Formalizing the LLL Basis Reduction Algorithm and the LLL Factorization Algorithm in Isabelle/HOL
The Use of Lemmas in the Model Elimination Procedure
MathSAT: Tight Integration of SAT and Mathematical Decision Procedures
On the Formalization of Theories
Computing Expected Visiting Times and Stationary Distributions in Markov Chains: Fast and Accurate
Hilbert's Tenth Problem is of Unification Type Zero
Evaluating Winding Numbers and Counting Complex Roots Through Cauchy Indices in Isabelle/HOL
Automated Reasoning in Differential Geometry and Mechanics Using the Characteristic Set Method. Part II. Mechanical Theorem Proving
On Computer-Assisted Proofs in Ordinal Number Theory
Proof Complexity of Modal Resolution
Proof Pearl: A Formal Proof of Dally and Seitz' Necessary and Sufficient Condition for Deadlock-Free Routing in Interconnection Networks
Short Proofs of the Pigeonhole Formulas Based on the Connection Method
The Unification Hierarchy is Undecidable
The Problem of Determining the Size of a Complete Set of Reductions
A Disjunctive Positive Refinement of Model Elimination and its Application to Subsumption Deletion
External Rewriting for Skeptical Proof Assistants
A Comparison of Mizar and Isar
Default Reasoning by Deductive Planning
A Decision Procedure for Linear "Big O" Equations
Modifying LOTOS Specifications by Means of Automatable Formula-Based Integrations
Formalising $\varSigma$-Protocols and Commitment Schemes Using CryptHOL
On the Complexity of Nested-Object Matching
Solving a problem with GeoGebra current possibilities and limits of CAS tools
System-Level Non-interference of Constant-Time Cryptography. Part II: Verified Static Analysis and Stealth Memory
Formalizing an Analytic Proof of the Prime Number Theorem
Formal Proofs of Rounding Error Bounds - With Application to an Automatic Positive Definiteness Check
Automated Synthesis of Recursive Programs from a forall-exists Logical Specification
On Modern Clause-Learning Satisfiability Solvers
The ILTP Problem Library for Intuitionistic Logic
General Clauses for SAT-Based Proof Search in Intuitionistic Propositional Logic
A New Default Theories Compilation for MSP-Entailment
Decision Procedures for Elementary Sublanguages of Set Theory: XII. Multilevel Syllogistic Extended with Singleton and Choice Operators
Proof Sytrategies in Linear Logic
The CADE-11 Competitions: A Personal View
First Order Stålmarck
Automatically Identifying the Asymptotic Behavior of Nonlinear Singularly Perturbed Boundary Value Problems
A Tribute to Woody Bledsoe
Schematic Refutations of Formula Schemata
View Updates in Stratified Disjunctive Databases
Mathematical Induction in Otter-Lambda
Solving Quantifier-Free First-Order Constraints Over Finite Sets and Binary Relations
Procedural Representation of CIC Proof Terms
A Formally Verified Proof of the Central Limit Theorem
Semantically-Guided Goal-Sensitive Reasoning: Model Representation
Any Ground Associative-Commutative Theory Has a Finite Canonical System
A Decision Procedure for Combinations of Propositional Temporal Logic and Other Specialized Theories
Preface: Selected Extended Papers from Interactive Theorem Proving 2018
General E -unification with Eager Variable Elimination and a Nice Cycle Rule
Tableaux for Logic Programming
DISCOUNT - A Distributed and Learning Equational Prover
Backdoor Sets for DLL Subsolvers
Strict computability models over categories and presheaves
Intuitionistic Modal Logic: A 15-year retrospective
Algebraic representations of some kinds of cocontinuous lattices
Formal semantics for perceptual classification
Transfer Results for Hybrid Logic. Part I: The Case Without Satisfaction Operators
Logics for reasoning about degrees of confirmation
A Modal Perspective on Path Constraints
Arg2P: an argumentation framework for explainable intelligent systems
Preservation by fibring of the finite model property
Jónsson-style canonicity for ALBA-inequalities
Characterizing Interpolation Pairs in Infinitary Graded Logics
Efficient Verified Programs in a Typed Theory with Mixed Constructivity
Two-to-one structures
Sustainable goal-oriented smart environments: a declarative programming approach
Logical Precision in Concept Lattices
Projective classes as images of accessible functors
Avicenna's logics with sentence-type terms: 1. Wholly muttaṣil syllogisms
Reasoning in social settings
Abstraction and Ontology: Questions as Propositional Abstracts in Type Theory with Records
On the Turing Degrees of Weakly Computable Real Numbers
A bilateral Hilbert-style investigation of 2-intuitionistic logic
A temporal argumentation approach to cooperative planning using dialogues
Editorial: The Possibility of Generating True Conjectures