| Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
| 1 | Jens Otten |
nanoCoP: A Non-clausal Connection Prover.  |
IJCAR  |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Sumit Gulwani |
Programming by Examples: Applications, Algorithms, and Ambiguity Resolution. |
IJCAR |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Xincai Gu, Taolue Chen, Zhilin Wu |
A Complete Decision Procedure for Linearly Compositional Separation Logic with Data Constraints. |
IJCAR |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Francesco Alberti, Silvio Ghilardi, Elena Pagani |
Counting Constraints in Flat Array Fragments. |
IJCAR |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Stephan Schulz 0001, Martin Möhrmann |
Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving. |
IJCAR |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Laura Bozzelli, Alberto Molinari, Angelo Montanari, Adriano Peron, Pietro Sala |
Interval Temporal Logic Model Checking: The Border Between Good and Bad HS Fragments. |
IJCAR |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Martin Bromberger, Christoph Weidenbach |
Fast Cube Tests for LIA Constraint Solving. |
IJCAR |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Kshitij Bansal, Andrew Reynolds 0001, Clark W. Barrett, Cesare Tinelli |
A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT. |
IJCAR |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrew Reynolds 0001, Jasmin Christian Blanchette, Simon Cruanes, Cesare Tinelli |
Model Finding for Recursive Functions in SMT. |
IJCAR |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Yoni Zohar, Anna Zamansky |
Gen2sat: An Automated Tool for Deciding Derivability in Analytic Pure Sequent Calculi. |
IJCAR |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Gabriel Ebner, Stefan Hetzl, Giselle Reis, Martin Riener, Simon Wolfsteiner, Sebastian Zivota |
System Description: GAPT 2.0. |
IJCAR |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Jeremy E. Dawson, James Brotherston, Rajeev Goré |
Machine-Checked Interpolation Theorems for Substructural Logics Using Display Calculi. |
IJCAR |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Ting Gan, Liyun Dai, Bican Xia, Naijun Zhan, Deepak Kapur, Mingshuai Chen |
Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF. |
IJCAR |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Takuya Matsuzaki, Hidenao Iwane, Munehiro Kobayashi, Yiyang Zhan, Ryoya Fukasaku, Jumma Kudo, Hirokazu Anai, Noriko H. Arai |
Race Against the Teens - Benchmarking Mechanized Math on Pre-university Problems. |
IJCAR |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Jasmin Christian Blanchette, Mathias Fleury, Christoph Weidenbach |
A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality. |
IJCAR |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Lars Hupel, Viktor Kuncak |
Translating Scala Programs to Isabelle/HOL - System Description. |
IJCAR |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Takahito Aoto 0001, Kentaro Kikuchi |
Nominal Confluence Tool. |
IJCAR |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Arnon Avron |
A Logical Framework for Developing and Mechanizing Set Theories. |
IJCAR |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Revantha Ramanayake |
Inducing Syntactic Cut-Elimination for Indexed Nested Sequents. |
IJCAR |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | André Platzer |
Logic & Proofs for Cyber-Physical Systems. |
IJCAR |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Hans de Nivelle |
Subsumption Algorithms for Three-Valued Geometric Resolution. |
IJCAR |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Diana Costa 0001, Manuel A. Martins 0001 |
A Tableau System for Quasi-Hybrid Logic. |
IJCAR |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Roberto Sebastiani |
Colors Make Theories Hard. |
IJCAR |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Benjamin Kiesl, Martina Seidl, Hans Tompits, Armin Biere |
Super-Blocked Clauses. |
IJCAR |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Florian Frohn, Matthias Naaf, Jera Hensel, Marc Brockschmidt, Jürgen Giesl |
Lower Runtime Bounds for Integer Programs. |
IJCAR |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Michael Färber 0002, Chad E. Brown |
Internal Guidance for Satallax. |
IJCAR |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | David M. Cerna, Alexander Leitsch |
Schematic Cut Elimination and the Ordered Pigeonhole Principle. |
IJCAR |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Cláudia Nalon, Ullrich Hustadt, Clare Dixon |
: A Resolution-Based Prover for Multimodal K. |
IJCAR |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Nicola Olivetti, Ashish Tiwari 0001 (eds.) |
Automated Reasoning - 8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings |
IJCAR |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Joseph Boudou |
Complexity Optimal Decision Procedure for a Propositional Dynamic Logic with Parallel Composition. |
IJCAR |
2016 |
DBLP DOI BibTeX RDF |
|
| 1 | Marijn Heule, Martina Seidl, Armin Biere |
A Unified Proof System for QBF Preprocessing. |
IJCAR |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | David Carral, Cristina Feier, Bernardo Cuenca Grau, Pascal Hitzler, Ian Horrocks 0001 |
EL-ifying Ontologies. |
IJCAR |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Laura Bozzelli, César Sánchez 0001 |
Visibly Linear Temporal Logic. |
IJCAR |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Olaf Beyersdorff, Leroy Chew |
The Complexity of Theorem Proving in Circumscription and Minimal Entailment. |
IJCAR |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Ori Lahav 0001, Yoni Zohar |
SAT-Based Decision Procedure for Analytic Pure Sequent Calculi. |
IJCAR |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Matthias Horbach, Viorica Sofronie-Stokkermans |
Locality Transfer: From Constrained Axiomatizations to Reachability Predicates. |
IJCAR |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Andreas Steigmiller, Birte Glimm, Thorsten Liebig |
Coupling Tableau Algorithms for Expressive Description Logics with Completion-Based Saturation Procedures. |
IJCAR |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Wenhui Zhang |
QBF Encoding of Temporal Properties and QBF-Based Verification. |
IJCAR |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev Goré, Kerry Olesen, Jimmy Thomson 0001 |
Implementing Tableau Calculi Using BDDs: BDDTab System Description. |
IJCAR |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Guy Avni, Orna Kupferman, Tami Tamir |
From Reachability to Temporal Specifications in Cost-Sharing Games. |
IJCAR |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Jasmin Christian Blanchette, Andrei Popescu 0001, Dmitriy Traytel |
Unified Classical Logic Completeness - A Coinductive Pearl. |
IJCAR |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Paula Daniela Chocron, Pascal Fontaine, Christophe Ringeissen |
A Gentle Non-disjoint Combination of Satisfiability Procedures. |
IJCAR |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Stefan Hetzl, Alexander Leitsch, Giselle Reis, Janos Tapolczai, Daniel Weller 0001 |
Introducing Quantified Cuts in Logic with Equality. |
IJCAR |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Vivek Nigam, Giselle Reis, Leonardo Lima 0001 |
Quati: An Automated Tool for Proving Permutation Lemmas. |
IJCAR |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Jean-Baptiste Jeannin, André Platzer |
dTL2: Differential Temporal Dynamic Logic with Nested Temporalities for Hybrid Systems. |
IJCAR |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Serenella Cerrito, Amélie David 0001, Valentin Goranko |
Optimal Tableaux-Based Decision Procedure for Testing Satisfiability in the Alternating-Time Temporal Logic ATL+. |
IJCAR |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Véronique Cortier |
Electronic Voting: How Logic Can Help. |
IJCAR |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Daniel Gorín, Dirk Pattinson, Lutz Schröder, Florian Widmann, Thorsten Wißmann |
Cool - A Generic Reasoner for Coalgebraic Hybrid Logics (System Description). |
IJCAR |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Joseph Boudou, Andreas Fellner, Bruno Woltzenlogel Paleo |
Skeptik: A Proof Compression System. |
IJCAR |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Michael Beeson, Larry Wos |
OTTER Proofs in Tarskian Geometry. |
IJCAR |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Aleksandar Zeljic, Christoph M. Wintersteiger, Philipp Rümmer |
Approximations for Model Construction. |
IJCAR |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Stéphane Demri, Deepak Kapur, Christoph Weidenbach (eds.) |
Automated Reasoning - 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 19-22, 2014. Proceedings |
IJCAR |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Cláudia Nalon, João Marcos 0001, Clare Dixon |
Clausal Resolution for Modal Logics of Confluence. |
IJCAR |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Rüdiger Ehlers, Martin Lange |
A Tool That Incrementally Approximates Finite Satisfiability in Full Interval Temporal Logic. |
IJCAR |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Fabio Papacchini, Renate A. Schmidt |
Terminating Minimal Model Generation Procedures for Propositional Modal Logics. |
IJCAR |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Aaron Stump, Geoff Sutcliffe, Cesare Tinelli |
StarExec: A Cross-Community Infrastructure for Logic Solving. |
IJCAR |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Jens Otten |
MleanCoP: A Connection Prover for First-Order Modal Logic. |
IJCAR |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev Goré, Jimmy Thomson 0001, Jesse Wu |
A History-Based Theorem Prover for Intuitionistic Propositional Logic Using Global Caching: IntHistGC System Description. |
IJCAR |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Björn Lellmann |
Axioms vs Hypersequent Rules with Context Restrictions: Theory and Applications. |
IJCAR |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Peter Baumgartner 0001, Joshua Bax, Uwe Waldmann |
Finite Quantification in Hierarchic Theorem Proving. |
IJCAR |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Adam Pease, Stephan Schulz 0001 |
Knowledge Engineering for Large Ontologies with Sigma KEE 3.0. |
IJCAR |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Mnacho Echenim, Nicolas Peltier, Sophie Tourret |
A Rewriting Strategy to Generate Prime Implicates in Equational Logic. |
IJCAR |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev Goré |
And-Or Tableaux for Fixpoint Logics with Converse: LTL, CTL, PDL and CPDL. |
IJCAR |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Ismail Ilkan Ceylan, Rafael Peñaloza |
The Bayesian Description Logic ${\mathcal{BEL}}$. |
IJCAR |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Patrick Koopmann, Renate A. Schmidt |
Count and Forget: Uniform Interpolation of $\mathcal{SHQ}$ -Ontologies. |
IJCAR |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Thomas Ströder, Jürgen Giesl, Marc Brockschmidt, Florian Frohn, Carsten Fuhs, Jera Hensel, Peter Schneider-Kamp |
Proving Termination and Memory Safety for Programs with Pointer Arithmetic. |
IJCAR |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Fredrik Lindblad |
A Focused Sequent Calculus for Higher-Order Logic. |
IJCAR |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Nicola Olivetti, Gian Luca Pozzato |
NESCOND: An Implementation of Nested Sequent Calculi for Conditional Logics. |
IJCAR |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Carlos Ansótegui, Maria Luisa Bonet, Jesús Giráldez-Cru, Jordi Levy |
The Fractal Dimension of SAT Formulas. |
IJCAR |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Jürgen Giesl, Marc Brockschmidt, Fabian Emmes, Florian Frohn, Carsten Fuhs, Carsten Otto, Martin Plücker, Peter Schneider-Kamp, Thomas Ströder, Stephanie Swiderski, René Thiemann |
Proving Termination of Programs Automatically with AProVE. |
IJCAR |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Josh Berdine, Nikolaj S. Bjørner |
Computing All Implied Equalities via SMT-Based Partition Refinement. |
IJCAR |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Thomas Sternagel, Harald Zankl |
KBCV - Knuth-Bendix Completion Visualizer. |
IJCAR |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Taus Brock-Nannestad, Carsten Schürmann 0001 |
Truthful Monadic Abstractions. |
IJCAR |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Daniel Kühlwein, Twan van Laarhoven, Evgeni Tsivtsivadze, Josef Urban, Tom Heskes |
Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics. |
IJCAR |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Pierre-Cyrille Héam, Vincent Hugot, Olga Kouchnarenko |
From Linear Temporal Logic Properties to Rewrite Propositions. |
IJCAR |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Fabian Emmes, Tim Enger, Jürgen Giesl |
Proving Non-looping Non-termination Automatically. |
IJCAR |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Siva Anantharaman, Serdar Erbatur, Christopher Lynch, Paliath Narendran, Michaël Rusinowitch |
Unification Modulo Synchronous Distributivity. |
IJCAR |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Mélanie Jacquel, Karim Berkani, David Delahaye, Catherine Dubois |
Tableaux Modulo Theories Using Superdeduction - An Application to the Verification of B Proof Rules with the Zenon Automated Theorem Prover. |
IJCAR |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Yuri V. Matiyasevich |
Enlarging the Scope of Applicability of Successful Techniques for Automated Reasoning in Mathematics. |
IJCAR |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Nikolaj S. Bjørner |
Taking Satisfiability to the Next Level with Z3 - (Abstract). |
IJCAR |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Pascal Fontaine, Stephan Merz, Christoph Weidenbach |
Combination of Disjoint Theories: Beyond Decidability. |
IJCAR |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Jan-David Quesel, André Platzer |
Playing Hybrid Games with KeYmaera. |
IJCAR |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Thomas Raths, Jens Otten |
The QMLTP Problem Library for First-Order Modal Logics. |
IJCAR |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Matej Urbas, Mateja Jamnik |
Diabelli: A Heterogeneous Proof System. |
IJCAR |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Andreas Steigmiller, Thorsten Liebig, Birte Glimm |
Extended Caching, Backjumping and Merging for Expressive Description Logics. |
IJCAR |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Sicun Gao, Jeremy Avigad, Edmund M. Clarke |
δ-Complete Decision Procedures for Satisfiability over the Reals. |
IJCAR |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Simon Foster 0001, Georg Struth |
Automated Analysis of Regular Algebra. |
IJCAR |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Roberto Sebastiani, Silvia Tomasi |
Optimization in SMT with ${\mathcal LA}$ (ℚ) Cost Functions. |
IJCAR |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Robert Nieuwenhuis |
SAT and SMT Are Still Resolution: Questions and Challenges. |
IJCAR |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrej Spielmann, Viktor Kuncak |
Synthesis for Unbounded Bit-Vector Arithmetic. |
IJCAR |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Alwen Tiu |
Stratification in Logics of Definitions. |
IJCAR |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | François Bobot, Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala, Assia Mahboubi, Alain Mebsout, Guillaume Melquiond |
A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic. |
IJCAR |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Moshe Emmer, Zurab Khasidashvili, Konstantin Korovin, Christoph Sticksel, Andrei Voronkov |
EPR-Based Bounded Model Checking at Word Level. |
IJCAR |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Boris Konev, Michel Ludwig, Frank Wolter |
Logical Difference Computation with CEX2.5. |
IJCAR |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Stefan Borgwardt, Felix Distel, Rafael Peñaloza |
How Fuzzy Is My Fuzzy Description Logic? |
IJCAR |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Frank S. de Boer, Marcello M. Bonsangue, Jurriaan Rot |
Automated Verification of Recursive Programs with Pointers. |
IJCAR |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Conrad Rau, David Sabel, Manfred Schmidt-Schauß |
Correctness of Program Transformations as a Termination Problem. |
IJCAR |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrew M. Marshall, Paliath Narendran |
New Algorithms for Unification Modulo One-Sided Distributivity and Its Variants. |
IJCAR |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Stephan Falke 0001, Deepak Kapur |
Rewriting Induction + Linear Arithmetic = Decision Procedure. |
IJCAR |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Dejan Jovanovic, Leonardo Mendonça de Moura |
Solving Non-linear Arithmetic. |
IJCAR |
2012 |
DBLP DOI BibTeX RDF |
|
![[Valid RSS]](Pics/valid-rss.png "Validate my RSS feed")
data released under the ODC-BY 1.0 license