Stem intuitionist$ (all stems)

67 papers:

FoSSaCS-2015-SchubertUZ #first-order #logic #on the

On the Mints Hierarchy in First-Order Intuitionistic Logic (AS, PU, KZ), pp. 451–465.

PPDP-2015-Brock-Nannestad #logic

Computation in focused intuitionistic logic (TBN, NG, DG), pp. 43–54.

CSL-2015-BaazF #logic

Elementary Elimination of Prenex Cuts in Disjunction-free Intuitionistic Logic (MB, CGF), pp. 94–109.

CSL-2015-Berardi #comprehension #higher-order #induction

Classical and Intuitionistic Arithmetic with Higher Order Comprehension Coincide on Inductive Well-Foundedness (SB), pp. 343–358.

LICS-2015-BaazLR #complexity #proving

A Note on the Complexity of Classical and Intuitionistic Proofs (MB, AL, GR), pp. 657–666.

IJCAR-2014-GoreTW #logic #proving #theorem proving #using

A History-Based Theorem Prover for Intuitionistic Propositional Logic Using Global Caching: IntHistGC System Description (RG, JT, JW), pp. 262–268.

LICS-CSL-2014-GuenotS #logic #normalisation #symmetry

Symmetric normalisation for intuitionistic logic (NG, LS), p. 10.

RTA-TLCA-2014-BerardiS #theorem

Ramsey Theorem as an Intuitionistic Property of Well Founded Relations (SB, SS), pp. 93–107.

FoSSaCS-2013-Strassburger #logic

Cut Elimination in Nested Sequents for Intuitionistic Modal Logics (LS), pp. 209–224.

CADE-2013-GoreT #logic

An Improved BDD Method for Intuitionistic Propositional Logic: BDDIntKt System Description (RG, JT), pp. 275–281.

CSL-2013-CloustonDGT #calculus #linear #logic

Annotation-Free Sequent Calculi for Full Intuitionistic Linear Logic (RC, JED, RG, AT), pp. 197–214.

LICS-2013-LiangM #logic

Unifying Classical and Intuitionistic Logics for Computational Control (CL, DM), pp. 283–292.

CSL-2012-LeitschRP #logic #towards

Towards CERes in intuitionistic logic (AL, GR, BWP), pp. 485–499.

IJCAR-2012-GoreT #automation #logic #reasoning

BDD-Based Automated Reasoning for Propositional Bi-Intuitionistic Tense Logics (RG, JT), pp. 301–315.

PPDP-2011-ToninhoCP #linear #type system

Dependent session types via intuitionistic linear type theory (BT, LC, FP), pp. 161–172.

CADE-2011-GalmicheM

A Connection-Based Characterization of Bi-intuitionistic Validity (DG, DM), pp. 268–282.

PPDP-2010-BaillotH #linear #logic #type inference

Type inference in intuitionistic linear logic (PB, MH), pp. 219–230.

CSL-2010-Chaudhuri #logic

Classical and Intuitionistic Subexponential Logics Are Equally Expressive (KC), pp. 185–199.

LICS-2010-Herbelin #logic #markov #principle

An Intuitionistic Logic that Proves Markov’s Principle (HH), pp. 50–56.

CIAA-J-2008-TsayW09 #automation #composition #reasoning

Automated Compositional Reasoning of Intuitionistically Closed Regular Properties (YKT, BYW), pp. 747–762.

CADE-2009-McLaughlinP #performance #proving #theorem proving

Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method (SM, FP), pp. 230–244.

CSL-2009-FerreiraO #functional #linear #logic

Functional Interpretations of Intuitionistic Linear Logic (GF, PO), pp. 3–19.

FLOPS-2008-AbelCD #algebra #on the #proving #type system

On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory (AA, TC, PD), pp. 3–13.

CIAA-2008-TsayW #automation #composition #reasoning

Automated Compositional Reasoning of Intuitionistically Closed Regular Properties (YKT, BYW), pp. 36–45.

IJCAR-2008-Otten #agile #logic #performance #proving #theorem proving

leanCoP 2.0and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions) (JO), pp. 283–291.

CADE-2007-HeilalaP #bidirectional #logic

Bidirectional Decision Procedures for the Intuitionistic Propositional Modal Logic IS4 (SH, BP), pp. 116–131.

CSL-2007-FournierGGZ #logic

Classical and Intuitionistic Logic Are Asymptotically Identical (HF, DG, AG, MZ), pp. 177–193.

CSL-2007-LiangM #logic

Focusing and Polarization in Intuitionistic Logic (CL, DM), pp. 451–465.

TLCA-2007-Berardi #game studies #semantics

Semantics for Intuitionistic Arithmetic Based on Tarski Games with Retractable Moves (SB), pp. 23–38.

TLCA-2007-Boulme #calculus #refinement

Intuitionistic Refinement Calculus (SB), pp. 54–69.

TLCA-2007-Fiore #difference #linear #logic #modelling #multi

Differential Structure in Models of Multiplicative Biadditive Intuitionistic Linear Logic (MPF), pp. 163–177.

TLCA-2007-SantoMP #calculus #continuation #normalisation

Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi (JES, RM, LP), pp. 133–147.

TLCA-2005-Hermant #calculus #semantics

Semantic Cut Elimination in the Intuitionistic Sequent Calculus (OH), pp. 221–233.

CSL-2004-Maier #liveness #ltl #safety

Intuitionistic LTL and a New Characterization of Safety and Liveness (PM), pp. 295–309.

CSL-2003-MaksimovaV #calculus #complexity #problem

Complexity of Some Problems in Modal and Intuitionistic Calculi (LM, AV), pp. 397–412.

TLCA-2003-SantoP #calculus #multi

Permutative Conversions in Intuitionistic Multiary Sequent Calculi with Cuts (JES, LP), pp. 286–300.

CADE-2002-Egly #logic

Embedding Lax Logic into Intuitionistic Logic (UE), pp. 78–93.

LICS-2002-Simpson #modelling #recursion #set

Computational Adequacy for Recursive Types in Models of Intuitionistic Set Theory (AKS), pp. 287–298.

ICLP-2001-BanbaraKHT #linear #logic programming

Logic Programming in a Fragment of Intuitionistic Temporal Linear Logic (MB, KSK, TH, NT), pp. 315–330.

LICS-2001-KozenT #correctness #linear #logic

Intuitionistic Linear Logic and Partial Correctness (DK, JT), pp. 259–268.

FoSSaCS-2000-MaiettiPR #category theory #linear #modelling #type system

Categorical Models for Intuitionistic and Linear Type Theory (MEM, VdP, ER), pp. 223–237.

ICALP-2000-LuttgenM #modelling #semantics

Fully-Abstract Statecharts Semantics via Intuitionistic Kripke Models (GL, MM), pp. 163–174.

CL-2000-HarlandLW #logic #multi #proving

Goal-Directed Proof Search in Multiple-Conclusions Intuitionistic Logic (JH, TL, MW), pp. 254–268.

CSL-2000-BaazZ #fuzzy #logic #proving

Hypersequent and the Proof Theory of Intuitionistic Fuzzy Logic (MB, RZ), pp. 187–201.

TLCA-1999-Hasegawa #linear #logic

Logical Predicates for Intuitionistic Linear Type Theories (MH), pp. 198–212.

TLCA-1999-PolakowP #deduction #linear #logic

Natural Deduction for Intuitionistic Non-communicative Linear Logic (JP, FP), pp. 295–309.

PLILP-1997-GiacobazziS #abstract interpretation

Intuitionistic Implication in Abstract Interpretation (RG, FS), pp. 175–189.

CADE-1997-KornK #logic

Deciding Intuitionistic Propositional Logic via Translation into Classical Logic (DSK, CK), pp. 131–145.

CADE-1996-RitterPW

Proof-Terms for Classical and Intuitionistic Resolution (Extended Abstract) (ER, DJP, LAW), pp. 17–31.

CADE-1996-Voronkov #logic #similarity

Proof-Search in Intuitionistic Logic with Equality, or Back to Simultaneous Rigid E-Unification (AV), pp. 32–46.

CSL-1996-Yashin #logic #problem

New Intuitionistic Logical Constants: Undecidability of the Conservativsness Problem (ADY), pp. 460–471.

LICS-1996-DegtyarevV #decidability #logic #problem

Decidability Problems for the Prenex Fragment of Intuitionistic Logic (AD, AV), pp. 503–512.

TLCA-1995-Bierman #category theory #linear #logic #question #what

What is a Categorical Model of Intuitionistic Linear Logic? (GMB), pp. 78–93.

ICALP-1994-Brauner #logic

A Model of Intuitionistic Affine Logic From Stable Domain Theory (TB), pp. 340–351.

CADE-1994-RoyerQ #on the #query

On Intuitionistic Query Answering in Description Bases (VR, JQ), pp. 326–340.

ILPS-1994-Hui-Bon-Hoa

Intuitionistic Implication and Resolution (AHBH), pp. 409–423.

ILPS-1994-McCartyS #first-order #interpreter #logic #prolog

A PROLOG Interpreter for First-Order Intuitionistic Logic (LTM, LAS), p. 685.

CSL-1993-Gomolko #consistency #logic #nondeterminism #prolog

Negation as Inconsistency in PROLOG via Intuitionistic Logic (AG), pp. 128–138.

ICLP-1993-McCarty #higher-order #induction #logic #prolog #proving #source code

Proving Inductive Properties of Prolog Programs in Second-Order Intuitionistic Logic (LTM), pp. 44–63.

ILPS-1993-Hui-Bon-Hoa #constraints

An Intuitionistic Resolution Method for a Language Dealing with Scope Constraints (AHBH), p. 667.

TLCA-1993-BentonBPH #calculus #linear #logic

A Term Calculus for Intuitionistic Linear Logic (PNB, GMB, VdP, MH), pp. 75–90.

CADE-1992-Shankar #calculus #proving

Proof Search in the Intuitionistic Sequent Calculus (NS), pp. 522–536.

JICSLP-1992-GiordanoO #logic programming

Negation as Failure in Intuitionistic Logic Programming (LG, NO), pp. 431–445.

LICS-1991-HodasM #linear #logic programming

Logic Programming in a Fragment of Intuitionistic Linear Logic (JSH, DM), pp. 32–42.

LICS-1991-LincolnSS

Linearizing Intuitionistic Implication (PL, AS, NS), pp. 51–62.

NACLP-1990-BonnerM #logic programming

Adding Negation-as-Failure to Intuitionistic Logic Programming (AJB, LTM), pp. 681–703.

NACLP-1989-BonnerMV #database #logic #query

Expressing Database Queries with Intuitionistic Logic (AJB, LTM, KVV), pp. 831–850.