yusuke1997/dblp-id-title huggingface dataset:
Human and Unhuman Commonsense Reasoning
Safe Positive Induction in the Programming Logic TK
A Programming Logic for a Verified Structured Assembly Language
Semantic A-translations and Super-Consistency Entail Classical Cut Elimination
Program Tactics and Logic Tactics
Optimizing the AES S-Box using SAT
A Seligman-Style Tableau System
An Inductive Theorem Prover Based on Narrowing
Logican's Workbench
A Mechanised Semantics for HOL with Ad-hoc Overloading
Default Reasoning with a Constraint Resolution Principle
Feasibility as a gradual notion
A Formalised Lower Bound on Undirected Graph Reachability
On Reasoning about Access to Knowledge
ISAR: An Interactive System for Algebraic Implementation Proofs
Netlog - A Concept Oriented Logic Programming Language
Revisiting the Equivalence of Shininess and Politeness
Disjunctive Constraint Lambda Calculi
Labelled Superposition for PLTL
Smart Testing of Functional Programs in Isabelle
Reasoning about Translation Lookaside Buffers
Sequentialization of Parallel Logic Programs with Mode Analysis
On Closure under Complementation of Equational Tree Automata for Theories Extending AC
Regular Derivations in Basic Superposition-Based Calculi
Matching in the Description Logic FL0 with respect to General TBoxes
How to Universally Close the Existential Rule
Inferring Termination Conditions for Logic Programs Using Backwards Analysis
Opium - A High-level Debugging Environment
Incorporating Hypothetical Views and Extended Recursion into SQL Database Systems
NP-Completeness Results for Deductive Problems on Stratified Terms
MULTILOG: A System for Axiomatizing Many-valued Logics
Completeness and Decidability in Sequence Logic
fCube: An Efficient Prover for Intuitionistic Propositional Logic
Fine Grained SMT Proofs for the Theory of Fixed-Width Bit-Vectors
A Sequent Calculus for a First Order Linear Temporal Logic with Explicit Time
Experiments with State-of-the-art Automated Provers on Problems in Tarskian Geometry
Deep Logic Program Transformation Using Abstract Interpretation
Towards computer-assisted proofs of parametric Andrews-Curtis simplifications, II
Automated Benchmarking of Incremental SAT and QBF Solvers
Nitpick: A Counterexample Generator for Isabelle/HOL Based on the Relational Model Finder Kodkod
Refinements and Extensions of Model Elimination
Towards Formal Reliability Analysis of Logistics Service Supply Chains using Theorem Proving
A Verified Theorem Prover Backend Supported by a Monotonic Library
Logic of Differentiable Logics: Towards a Uniform Semantics of DL
On Termination of Meta-Programs
Automatic Space Bound Analysis for Functional Programs with Garbage Collection
Automatic Combinability of Rewriting-Based Satisfiability Procedures
Automated Termination Analysis for Incompletely Defined Programs
Experimental Evaluation of Classical Automata Constructions
Cut Elimination for First Order Gödel Logic by Hyperclause Resolution
Polynomial Loops: Beyond Termination
On CTL* with Graded Path Modalities
Confluence of Non-Left-Linear TRSs via Relative Termination
Long-Distance Resolution: Proof Generation and Strategy Extraction in Search-Based QBF Solving
Extending a Resolution Prover for Inequalities on Elementary Functions
Certification of Tail Recursive Bubble-Sort in Theorema and Coq
Gödel Logics - A Survey
Polar: A Framework for Proof Refactoring
Logic for Programming, Artificial Intelligence, and Reasoning, 14th International Conference, LPAR 2007, Yerevan, Armenia, October 15-19, 2007, Proceedings
Reasoning About Prescription and Description Using Prioritized Default Rules
Some Considerations on the Logic PfD
Logic for Programming, Artificial Intelligence, and Reasoning, 8th International Conference, LPAR 2001, Havana, Cuba, December 3-7, 2001, Proceedings
The Thousands of Models for Theorem Provers (TMTP) Model Library - First Steps
Theorem Provers For Every Normal Modal Logic
Extensions to the Estimation Calculus
BRAVE: An OR-Parallel Dialect of Prolog and its Application to Artificial Intelligence
Constructing Camin-Sokal Phylogenies Via Answer Set Programming
A Proof Search System for a Modal Substructural Logic Based on Labelled Deductive Systems
On Reducing Clause DataBase in Glucose
Logic for Programming, Artificial Intelligence, and Reasoning - 16th International Conference, LPAR-16, Dakar, Senegal, April 25-May 1, 2010, Revised Selected Papers
Weighted Answer Sets and Applications in Intelligence Analysis
Linear 0-1 Inequalities and Extended Clauses
A Procedure for Automatic Proof Nets Construction
Controlling Redundancy in Large Search Spaces: Argonne-Style Theorem Proving Through the Years
Behavioural Constructor Implementation for Regular Algebras
A Declarative Debugging Environment for DATALOG
Extensions of Non-standard Inferences to Descriptions Logics with Transitive Roles
When Are Two Gossips the Same?
Combining Supervaluation and Degree Based Reasoning Under Vagueness
Animating TLA Specifications
Implementation of Prolog as Binary Definite Programs
Andorra Model Revised: Introducing Nested Domain Variables and a Targeted Search
Deep Reinforcement Learning for Synthesizing Functions in Higher-Order Logic
Logical Operational Semantics of Parlog. Part II: Or-Parallelism
Finding Finite Herbrand Models
Solving Combinatorial Problems with Regular Local Search Algorithms
A Theory of Satisfiability-Preserving Proofs in SAT Solving
Polarizing Double-Negation Translations
Modular Multiset Rewriting
Reasoning with Concept Diagrams about Antipatterns
TIP: Tools for Inductive Provers
Efficient First Order Functional Program Interpreter with Time Bound Certifications
Gödel logics and the fully boxed fragment of LTL
Implementing an Efficient SAT Solver for a Probabilistic Description Logic
A Computer Environment for Writing Ordinary Mathematical Proofs
Translating HOL-Light proofs to Coq
Lookahead-Based SMT Solving
Alternate Semantics of the Guarded Conditional
Efficient SAT-Based Encodings of Conditional Cardinality Constraints
Using an Abstract Representation to Specialize Functional Logic Programs
On Conditional Rewrite Systems with Extra Variables and Deterministic Logic Programs
Second-Order Principles in Specification Languages for Object-Oriented Programs
A Local System for Intuitionistic Logic
LTL with Arithmetic and its Applications in Reasoning about Hierarchical Systems
Verification Condition Generation Via Theorem Proving
Verification of Concurrent Programs Using Trace Abstraction Refinement
Complexity, Graphs, and the Dependency Pair Method
Integration of a Software Model Checker into Isabelle
On Module-Based Abstraction and Repair of Behavioral Programs
A Trichotomy in the Complexity of Propositional Circumscription
Enhancing Search-Based QBF Solving by Dynamic Blocked Clause Elimination
A PVS Proof Obligation Generator for Lustre Programs
Permutation Problems and Channelling Constraints
A Note on Universal Measures for Weak Implicit Computational Complexity
FIDO: Finite Domain Consistency Techniques in Logic Programming
Verifying SQL queries using theories of tables and relations
Reasoning Using Knots
RACCOON: A Connection Reasoner for the Description Logic ALC
On Symbolic Derivatives and Transition Regexes
Towards Efficient Metaquery Generator
Extended Canonicity of Certain Topological Properties of Set Spaces
Cartesian Reachability Logic: A Language-parametric Logic for Verifying k-Safety Properties
Maintenance of Formal Software Developments by Stratified Verification
An Interactive SMT Tactic in Coq using Abductive Reasoning
Symbolic WS1S
Treating Enhanced Entity Relationship Models in a Declarative Style
An Extension of BDI CTL with Functional Dependencies and Components
Monotone AC-Tree Automata
An Epistemic Event Calculus for ASP-based Reasoning About Knowledge of the Past, Present and Future
Playing with the Maximum-Flow Problem
Relating Innermost, Weak, Uniform and Modular Termination of Term Rewriting Systems
Synthesis of Trigger Properties
On the Complexity of the Bernays-Schönfinkel Class with Datalog
Symmetry Breaking for Maximum Satisfiability
An Incremental Approach to Abstraction-Carrying Code
Tableau-Based Revision over SHIQ TBoxes
Leo-III Version 1.1 (System description)
The Inverse Method for the Logic of Bunched Implications
Optimized Translation of Multi Modal Logic into Predicate Logic
Implementing Efficient Resource Management for Linear Logic Programming
Incremental Tabling for Query-Driven Propagation of Logic Program Updates
Defining Privacy Is Supposed to Be Easy
Complete Pruning Methods and a Practical Search Strategy for SOL
Automated Reasoning for Mizar: Artificial Intelligence through Knowledge Exchange
Herbrand's Theorem for Prenex Gödel Logic and its Consequences for Theorem Proving
Proof Development with Omega-MEGA: sqrt(2) Is Irrational
Enriched µ-Calculus Pushdown Module Checking
Preferential Description Logics
Formalization of some central theorems in combinatorics of finite sets
A Generic Logic Environment
An Algorithm for Enumerating Maximal Models of Horn Theories with an Application to Modal Logics
Improving Resource-Unaware SAT Solvers
Rewriting Environment for Arithmetic Circuit Verification
Automated Synthesis of Decision Lists for Polynomial Specifications over Integers
Variable Dependencies of Quantified CSPs
Forgetting Concept and Role Symbols in $\mathcal{ALCH}$ -Ontologies
Functional Correctness Proofs of Encryption Algorithms
Automata for Positive Core XPath Queries on Compressed Documents
Relaxing Synchronization Constraints in Behavioral Programs
Implicit Computational Complexity of Subrecursive Definitions and Applications to Cryptographic Proofs
RISC-CLP(CF) Constraint Logic Programming over Complex Functions
Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: A Comparative Analysis
Loop Analysis by Quantification over Iterations
An Isomorphism between a Fragment of Sequent Calculus and an Extension of Natural Deduction
Counting the Number of Equivalent Binary Resolution Proofs
Analysis of Polymorphically Typed Logic Programs Using ACI-Unification
Nonmonotonic Description Logic Programs: Implementation and Experiments
A Tool for Reasoning about Trust and Belief
Proof rules for the dialogical logic N
Note on Deduction Theorems in Contraction-Free Logics
SAT Modulo Intuitionistic Implications
Cut-Elimination: Experiments with CERES
On Computing Fixpoints in Well-Structured Regular Model Checking, with Applications to Lossy Channel Systems
Dynamics of Argumentation Systems: A Basic Theory
Efficient and Verified Continuous Double Auctions
A Labelled Sequent Calculus for Intuitionistic Public Announcement Logic
VIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic
Solving Geometry Problems Using a Combination of Symbolic and Numerical Reasoning
Keep me out of the loop: a more flexible choreographic projection
Logic for Programming, Artificial Intelligence, and Reasoning, 13th International Conference, LPAR 2006, Phnom Penh, Cambodia, November 13-17, 2006, Proceedings
Directed Automated Theorem Proving
Expressive Path Queries on Graphs with Data
Automatic Certification of Heap Consumption
Transforming Conditional Rewrite Systems with Extra Variables into Unconditional Systems
Congruence Closure with Integer Offsets
Rewriting and Inductive Reasoning
A New Model Construction for the Polymorphic Lambda Calculus
The TPTP Typed First-Order Form with Arithmetic
Focusing Strategies in the Sequent Calculus of Synthetic Connectives
Proofs About Lists Using Ellipsis
An Interpolation-based Compiler and Optimizer for Relational Queries (System design Report)
Abstract Domains and Solvers for Sets Reasoning
Another Complete Local Search Method for SAT
Verifying Pointer and String Analyses with Region Type Systems
(LIA) - Model Evolution with Linear Integer Arithmetic Constraints
Census Data Repair: a Challenging Application of Disjunctive Logic Programming
Saturation Up to Redundancy for Tableau and Sequent Calculi
Robotics, Temporal Logic and Stream Reasoning
Real-Time Memory Management for Prolog
A Mathematical Benchmark for Inductive Theorem Provers
Abox Satisfiability Reduced to Terminological Reasoning in Expressive Description Logics
Encoding Queues in Satisfiability Modulo Theories Based Bounded Model Checking
Partial Implicit Unfolding in the Davis-Putnam Procedure for Quantified Boolean Formulae
NACRE - A Nogood And Clause Reasoning Engine
Imogen: Focusing the Polarized Inverse Method for Intuitionistic Propositional Logic
Pruning Infinite Failure Branches in Programs with Occur-Check
Logic for Programming, Artificial Intelligence, and Reasoning, 15th International Conference, LPAR 2008, Doha, Qatar, November 22-27, 2008. Proceedings
Clausal Graph Tableaux for Hybrid Logic with Eventualities and Difference
Analyzing Multiple Conflicts in SAT: An Experimental Evaluation
A Logical Study on Qualitative Default Reasoning with Probabilities
Waste Reduction: Experiments in Sharing Clauses between Runs of a Portfolio of Strategies (Experimental Paper)
Practical Reasoning for Expressive Description Logics
TacticToe: Learning to Reason with HOL4 Tactics
Toward Optimal Radio Colorings of Hypercubes via SAT-solving
Consistency of Equational Enrichments
Computing Extensions of Default Logic - Preliminary Report
SAT-Based Minimization of Deterministic \omega -Automata
SEPIA - a Bases for Prolog Extensions
Decidable and Undecidable Fragments of Halpern and Shoham's Interval Temporal Logic: Towards a Complete Classification
On Interpolation in Existence Logics
Hardness of Preorder Checking for Basic Formalisms
Free Deduction: An Analysis of "Computations" in Classical Logic
Coloring Unit-Distance Strips using SAT
To Ackermann-ize or Not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in SMT ( EUF È T )
Ordinals and Knuth-Bendix Orders
Games and Model Checking for Guarded Logics
Efficient Negation Using Abstract Interpretation
Lazy Abstraction for Size-Change Termination
From SAT to Maximum Independent Set: A New Approach to Characterize Tractable Classes
LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, May 7-12, 2017
On Locally Checkable Properties
How to Decide Query Containment Under Constraints Using a Description Logic
Model Checking the First-Order Fragment of Higher-Order Fixpoint Logic
ABC: Algebraic Bound Computation for Loops
Scalable Probabilistic Routes
Local Temporal Logic is Expressively Complete for Cograph Dependence Alphabets
The Complexity of Clausal Fragments of LTL
Extending Compositional Message Sequence Graphs
A Relaxed Approach to Integrity and Inconsistency in Databases
Practical Querying of Temporal Data via OWL 2 QL and SQL: 2011
Label-Free Proof Systems for Intuitionistic Modal Logic IS5
Decidability, Introduction Rules and Automata
Operational and Epistemic Approaches to Protocol Analysis: Bridging the Gap
On Proof Schemata and Primitive Recursive Arithmetic
A Complete Cyclic Proof System for Inductive Entailments in First Order Logic
Free Logic and Infinite Constraint Networks
Quantified Boolean Formulas: Call the Plumber!
Program Logics for Homogeneous Meta-programming
Dafny: An Automatic Program Verifier for Functional Correctness
On the Complexity of Model Expansion
Matrix Interpretations for Polynomial Derivational Complexity of Rewrite Systems
Partial Backtracking in CDCL Solvers
Multi-objective Discounted Reward Verification in Graphs and MDPs
On the Notion of Vacuous Truth
Towards Practical Feasibility of Core Computation in Data Exchange
Approved Models for Normal Logic Programs
A First Order Extension of Stålmarck's Method
A Verification Environment for Sequential Imperative Programs in Isabelle/HOL
An Extensible Proof Text Editor
On a Proof-Theoretical Analysis of Sigma-1, 1-AC, Sigma-1, 1-DC and Delta-1, 1-CA
An Abstract Interpretation Approach to Termination of Logic Programs
On Finite Satisfiability of the Guarded Fragment with Equivalence or Transitive Guards
An ASP-based Approach for Boolean Networks Representation and Attractor Detection
SMTS: Distributed, Visualized Constraint Solving
Indexed Categories and Bottom-Up Semantics of Logic Programs
Induction Models on N
Uniform Rules and Dialogue Games for Fuzzy Logics
Extracting Inheritance Hierarchies from Prolog Programs: A System Based on the Inference of Type Relations
Logic for Programming, Artificial Intelligence, and Reasoning - 17th International Conference, LPAR-17, Yogyakarta, Indonesia, October 10-15, 2010. Proceedings
First-Order Interpolation and Interpolating Proof Systems
WAM Algebras - A Mathematical Study of Implementation, Part 2
Reasoning, Modeling, and Component-Based Technology
A compositional semantics for Repairable Fault Trees with general distributions
CERES in Many-Valued Logics
Controller Synthesis for MDPs and Frequency LTL \GU
Bunched Hypersequent Calculi for Distributive Substructural Logics
BCiC: A System for Code Authentication and Verification
Learning Techniques for Pseudo-Boolean Solving
Towards an Abstraction-Refinement Framework for Reasoning with Large Theories
Two-variable First-Order Logic with Counting in Forests
MegaLog - A Platform for Developing Knowledge Base Management Systems
LPAR-22 Workshop and Short Paper Proceedings, Awassa, Ethiopia, 16-21 November 2018
SPIKE, an Automatic Theorem Prover
Numeric Base Conversion with Rewriting
A Logic of Singly Indexed Arrays
Sometimes Hoarding is Harder than Cleaning: NP-hardness of Maximum Blocked-Clause Addition
Completeness for Flat Modal Fixpoint Logics
Combining Typing and Size Constraints for Checking the Termination of Higher-Order Conditional Rewrite Systems
The Completion of Typed Logic Programs and SLDNF-Resolution
One-Pass Tableaux for Computation Tree Logic
Disjunctive Deductive Databases
First-Order Logic as a Constraint Programming Language
A Simple Token Game and its Logic
Boolean Rings for Intersection-Based Satisfiability
Finding Small Proofs for Description Logic Entailments: Theory and Practice
Prolog Semantics for Measuring Space Consumption
On the Domain and Dimension Hierarchy of Matrix Interpretations
Non-Clausal Resolution and Superposition with Selection and Redundancy Criteria
ELPI: Fast, Embeddable, λProlog Interpreter
Solving Planning Problems by Partial Deduction
Atomic Cut Introduction by Resolution: Proof Structuring and Compression
Implementing Polymorphism in Zenon
SAT-Based Preprocessing for MaxSAT
Connection-Based Proof Construction in Non-commutative Logic
Qex: Symbolic SQL Query Explorer
Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015, Proceedings
Parallel Computation of Multiple Sets-of_Support
The Boundary between Decidable and Undecidable Fragments of the Fluent Calculus
A TLA+ Proof System
A Prolog-based Proof Tool for Type-Theory TA-lambda and Implicational Intuitionistic-Logic
Transforming and Analyzing Proofs in the CERES-System
Zap: Automated Theorem Proving for Software Analysis
Improving Context-Sensitive Dependency Pairs
Lemma Mining over HOL Light
Experiments on Infinite Model Finding in SMT Solving
Model Generation with Boolean Constraints
Logic for Programming, Artificial Intelligence, and Reasoning, 10th International Conference, LPAR 2003, Almaty, Kazakhstan, September 22-26, 2003, Proceedings
Instantiations, Zippers and EPR Interpolation
Concepts of Automata Construction from LTL
Verification, Testing, and Runtime Monitoring of Automotive Exhaust Emissions
Investigating Type-Certifying Compilation with Isabelle
Towards Smarter MACE-style Model Finders
On the Complexity of Disjunction and Explicit Definability Properties in Some Intermediate Logics
Aligators for Arrays (Tool Paper)
Proof Search in Nested Sequent Calculi
Independently Checkable Proofs from Decision Procedures: Issues and Progress
Improving Statistical Linguistic Algorithms for Parsing Mathematics
Covered Clause Elimination
SMT Solving over Finite Field Arithmetic
Left-Handed Completeness for Kleene algebra, via Cyclic Proofs
Efficient SAT Engines for Concise Logics: Accelerating Proof Search for Zero-One Linear Constraint Systems
Automated Theorem Proving by Translation to Description Logic
A Formal Proof of Dickson's Lemma in ACL2
Compositional Propositional Proofs
Model Checking Abstract State Machines with Answer Set Programming
The 8th International Workshop on the Implementation of Logics, IWIL 2010, Yogyakarta, Indonesia, October 9, 2011
Abductive Systems for Non-Monotonic Reasoning
Retractile Proof Nets of the Purely Multiplicative and Additive Fragment of Linear Logic
Objects in a Logic Programming Framework
Prover9 Unleashed: Automated Configuration for Enhanced Proof Discovery
Seminator: A Tool for Semi-Determinization of Omega-Automata
On Anti-Links
Using Program Synthesis for Program Analysis
Regular Expressions for Data Words
Stateful Premise Selection by Recurrent Neural Networks
The External Database in SICStus Prolog
Towards Probabilistic Knowledge Bases
Symmetry breaking in a new stable model search method
Reform Compilation for Nonlinear Recursion
Description Logics, Rules and Multi-context Systems
Have Spass with OCC1N g =
The Functions Provable by First Order Abstraction
Monitor-Based Statistical Model Checking for Weighted Metric Temporal Logic
The Dependency Pair Framework: Combining Techniques for Automated Termination Proofs
On Procedural Semantics of Metalevel Negation
On the Value of Antiprenexing
Querying Inconsistent Databases
Sequential, Parallel, and Quantified Updates of First-Order Structures
Equational Binary Decision Diagrams
Maximal Falsifiability - Definitions, Algorithms, and Applications
Searching for Invariants Using Temporal Resolution
A Monotonic Higher-Order Semantic Path Ordering
Extended Computation Tree Logic
On Strong Normalization of the Calculus of Constructions with Type-Based Termination
Going Polymorphic - TH1 Reasoning for Leo-III
Intuitionistic Multiplicative Proof Nets as Models of Directed Acyclic Graph Descriptions
Synchronizing Constrained Horn Clauses
Discounted Properties of Probabilistic Pushdown Automata
Moral Reasoning under Uncertainty
Cancellative Superposition Decides the Theory of Divisible Torsion-Free Abelian Groups
A Conditional Logical Framework
Graph Operations and Monadic Second-Order Logic: A Survey
Higher-Order Rigid E-Unification
Refining Unification with Abstraction
System Description: E 1.8
A Natural-style Prover in Theorema Using Sequent Calculus with Unit Propagation
General Model Theoretic Semantics for Higher-Order Horn Logic Programming
Multi-SLD Resolution
Improving Dependency Pairs
Treewidth: A Useful Marker of Empirical Hardness in Quantified Boolean Logic Encodings
Automated Theorem Proving Proof and Model Generation with Disconnection Tableaux
Extending a Verified Simplex Algorithm
How the Location of * Influences Complexity in Kleene Algebra with Tests
Yet Another Application for Topie: Verification of Mutual Exclusion Algorithms
Putting Newton into Practice: A Solver for Polynomial Equations over Semirings
An Order Theory Resolution Calculus
Focused Labeled Proof Systems for Modal Logic
On the Interaction of Inclusion Dependencies with Independence Atoms
Deciding Satisfiability of Positive Second Order Joinability Formulae
The Variable Hierarchy for the Lattice µ-Calculus
Procedural Semantics for Fuzzy Disjunctive Programs
Logic Programming with Bounded Quantifiers
Soundness and Completeness of Partial Deductions for Well-Founded Semantics
On Two Extensions of Abstract Categorial Grammars
A Characterization of Alternating Log Time by First Order Functional Programs
Fast Counting with Bounded Treewidth
Reveal: A Formal Verification Tool for Verilog Designs
Consistency Checking of Automata Functional Specifications
Learning What Others Know
Blocked Clauses in First-Order Logic
Automated Discovery of Simulation Between Programs
Complexity of Admissible Rules in the Implication-Negation Fragment of Intuitionistic Logic
Clause Elimination Procedures for CNF Formulas
Logic for Programming, Artificial Intelligence, and Reasoning - 18th International Conference, LPAR-18, Mérida, Venezuela, March 11-15, 2012. Proceedings
Data-Oblivious Stream Productivity
Application of Automated Deduction to the Search for Single Axioms for Exponent Groups
Automated Proof Compression by Invention of New Definitions