Stem formula$ (all stems)

295 papers:

ICSME-2015-JansenH #dataset #industrial #smell #spreadsheet

Code smells in spreadsheet formulas revisited on an industrial dataset (BJ, FH), pp. 372–380.

SCAM-2015-AivaloglouHH #dataset #scalability #spreadsheet

A grammar for spreadsheet formulas evaluated on two large datasets (EA, DH, FH), pp. 121–130.

ICALP-v1-2015-MouawadNPR #configuration management

Shortest Reconfiguration Paths in the Solution Space of Boolean Formulas (AEM, NN, VP, VR), pp. 985–996.

LATA-2015-Peltier #approach #reasoning

Reasoning on Schemas of Formulas: An Automata-Based Approach (NP), pp. 263–274.

CSL-2015-LehtinenQ

Deciding the First Levels of the Modal μ Alternation Hierarchy by Formula Construction (KL, SQ), pp. 457–471.

SAT-2015-ArifMM #axiom #performance

Efficient MUS Enumeration of Horn Formulae with Applications to Axiom Pinpointing (MFA, CM, JMS), pp. 324–342.

SAT-2015-IgnatievPM #satisfiability

SAT-Based Formula Simplification (AI, AP, JMS), pp. 287–298.

SAT-2015-IserMS #recognition

Recognition of Nested Gates in CNF Formulas (MI, NM, CS), pp. 255–271.

SAT-2015-NewshamLGLFC #evolution #named #satisfiability #visualisation

SATGraf: Visualizing the Evolution of SAT Formula Structure in Solvers (ZN, WL, VG, JHL, SF, KC), pp. 62–70.

DATE-2014-SeidlK #quantifier

Partial witnesses from preprocessed quantified Boolean formulas (MS, RK), pp. 1–6.

WRLA-2014-BaeM #infinity #model checking #using

Infinite-State Model Checking of LTLR Formulas Using Narrowing (KB, JM), pp. 113–129.

STOC-2014-FournierLMS #bound #matrix #multi

Lower bounds for depth 4 formulas computing iterated matrix multiplication (HF, NL, GM, SS), pp. 128–135.

STOC-2014-GavinskyMWW #approach #bound #complexity #composition #towards

Toward better formula lower bounds: an information complexity approach to the KRW composition conjecture (DG, OM, OW, AW), pp. 213–222.

STOC-2014-KayalLSS #bound

Super-polynomial lower bounds for depth-4 homogeneous arithmetic formulas (NK, NL, CS, SS), pp. 119–127.

STOC-2014-KayalSS #bound

A super-polynomial lower bound for regular arithmetic formulas (NK, CS, RS), pp. 146–153.

STOC-2014-KumarS #all about #reduction

The limits of depth reduction for arithmetic formulas: it’s all about the top fan-in (MK, SS), pp. 136–145.

STOC-2014-Rossman #distance

Formulas vs. circuits for small distance connectivity (BR), pp. 203–212.

LATA-2014-AleksandrowiczABB

Formulae for Polyominoes on Twisted Cylinders (GA, AA, GB, RB), pp. 76–87.

KEOD-2014-AkamaN #problem

Solving Query-answering Problems with If-and-Only-If Formulas (KA, EN), pp. 333–344.

KR-2014-BartholomewL #modelling #multi

Stable Models of Multi-Valued Formulas: Partial versus Total Functions (MB, JL).

KR-2014-HarrisonLY #semantics

The Semantics of Gringo and Infinitary Propositional Formulas (AJH, VL, FY).

KR-2014-ShenZ #canonical #logic programming #source code

Canonical Logic Programs are Succinctly Incomparable with Propositional Formulas (YS, XZ).

SIGIR-2014-LinGHTXL #layout #retrieval

A mathematics retrieval system for formulae in layout presentations (XL, LG, XH, ZT, YX, XL), pp. 697–706.

PLATEAU-2014-KoitzS #comparison #education #empirical #hybrid #programming language #visual notation

Empirical Comparison of Visual to Hybrid Formula Manipulation in Educational Programming Languages for Teenagers (RK, WS), pp. 21–30.

POPL-2014-ItzhakyBILNS #composition #effectiveness #reasoning

Modular reasoning about heap paths via effectively propositional formulas (SI, AB, NI, OL, AN, MS), pp. 385–396.

FSE-2014-HermansD #named #refactoring #spreadsheet

BumbleBee: a refactoring environment for spreadsheet formulas (FH, DD), pp. 747–750.

IJCAR-2014-AnsoteguiBGL #satisfiability

The Fractal Dimension of SAT Formulas (CA, MLB, JGC, JL), pp. 107–121.

LICS-CSL-2014-Munch-Maccagnoni #type system

Formulae-as-types for an involutive negation (GMM), p. 10.

SAT-2014-MiksaN #proving

Long Proofs of (Seemingly) Simple Formulas (MM, JN), pp. 121–137.

SAT-2014-SaetherTV #satisfiability

Solving MaxSAT and #SAT on Structured CNF Formulas (SHS, JAT, MV), pp. 16–31.

ICDAR-2013-AlkalaiBSL #analysis #identification

Improving Formula Analysis with Line and Mathematics Identification (MA, JBB, VS, XL), pp. 334–338.

ICDAR-2013-FurukoriYMSO #documentation

An OCR System with OCRopus for Scientific Documents Containing Mathematical Formulas (FF, SY, TM, KS, MO), pp. 1175–1179.

ICDAR-2013-LinGTBAS #detection #recognition

A Text Line Detection Method for Mathematical Formula Recognition (XL, LG, ZT, JBB, MA, VS), pp. 339–343.

ICDAR-2013-TangHF #analysis #approach #recognition

A Progressive Structural Analysis Approach for Handwritten Chemical Formula Recognition (PT, SCH, CWF), pp. 359–363.

TACAS-2013-BelovJM #preprocessor

Formula Preprocessing in MUS Extraction (AB, MJ, JMS), pp. 108–123.

STOC-2013-AgrawalSS

Quasi-polynomial hitting-set for set-depth-Δ formulas (MA, CS, NS), pp. 321–330.

STOC-2013-KomargodskiR #bound

Average-case lower bounds for formula size (IK, RR), pp. 171–180.

DLT-2013-Pin #regular expression

An Explicit Formula for the Intersection of Two Polynomials of Regular Languages (JÉP), pp. 31–45.

GCM-J-2012-Radke #graph #higher-order #monad

HR* Graph Conditions Between Counting Monadic Second-Order and Second-Order Graph Formulas (HR).

HILT-2013-Jackson #domain-specific language

Engineering domain-specific languages with formula 2.0 (EKJ), pp. 3–4.

CIKM-2013-JabbourSSU #approach

Mining-based compression approach of propositional formulae (SJ, LS, YS, TU), pp. 289–298.

CADE-2013-KovasznaiFB #quantifier

: A Tool for Polynomially Translating Quantifier-Free Bit-Vector Formulas into (GK, AF, AB), pp. 443–449.

CAV-2013-Marques-SilvaJB #set

Minimal Sets over Monotone Predicates in Boolean Formulae (JMS, MJ, AB), pp. 592–607.

SAT-2013-BubeckB #modelling #quantifier

Nested Boolean Functions as Models for Quantified Boolean Formulas (UB, HKB), pp. 267–275.

SAT-2013-LonsingEG #learning #performance #pseudo #quantifier

Efficient Clause Learning for Quantified Boolean Formulas via QBF Pseudo Unit Propagation (FL, UE, AVG), pp. 100–115.

DocEng-2012-MarinaiQ #game studies

Displaying chemical structural formulae in ePub format (SM, SQ), pp. 125–128.

DRR-2012-LinGTHL #documentation #embedded #identification #using

Identification of embedded mathematical formulas in PDF documents using SVM (XL, LG, ZT, XH, XL).

WRLA-2012-BaeM #locality #model checking

Model Checking LTLR Formulas under Localized Fairness (KB, JM), pp. 99–117.

ICSM-2012-BadameD #refactoring #spreadsheet

Refactoring meets spreadsheet formulas (SB, DD), pp. 399–409.

ICSM-2012-HermansPD #detection #smell #spreadsheet

Detecting code smells in spreadsheet formulas (FH, MP, AvD), pp. 409–418.

STOC-2012-AgrawalSSS #bound

Jacobian hits circuits: hitting-sets, lower bounds for depth-D occur-k formulas & depth-3 transcendence degree-k circuits (MA, CS, RS, NS), pp. 599–614.

STOC-2012-DvirMPY #branch #multi #source code

Separating multilinear branching programs and formulas (ZD, GM, SP, AY), pp. 615–624.

ICALP-v2-2012-AtseriasD #approximate #bound #quantifier

Degree Lower Bounds of Tower-Type for Approximating Formulas with Parity Quantifiers (AA, AD), pp. 67–78.

KR-2012-BartholomewL #modelling

Stable Models of Formulas with Intensional Functions (MB, JL).

KR-2012-BordeauxJSM #on the #quantifier

On Unit-Refutation Complete Formulae with Existentially Quantified Variables (LB, MJ, JPMS, PM).

SEKE-2012-LiuCL #concurrent #in the cloud

Singular Formulas for Compound Siphons, Complementary Siphons and Characteristic Vectors for Deadlock Prevention in Cloud Computing (GL, DYC, YNL), pp. 359–362.

SAC-2012-ChhelLGS #biology #multi #using

Minimum multiple characterization of biological data using partially defined boolean formulas (FC, FL, AG, FS), pp. 1399–1405.

SAC-2012-ZhaoHWA #constraints #diagrams #difference #equation #polynomial

Real solution formulas of cubic and quartic equations applied to generate dynamic diagrams with inequality constraints (TZ, HH, DW, PA), pp. 94–101.

ICLP-2012-LeeM #modelling #quantifier

Stable Models of Formulas with Generalized Quantifiers (Preliminary Report) (JL, YM), pp. 61–71.

LICS-2012-ChenD #quantifier

Decomposing Quantified Conjunctive (or Disjunctive) Formulas (HC, VD), pp. 205–214.

LICS-2012-KrebsS #first-order

Non-definability of Languages by Generalized First-order Formulas over (N, +) (AK, AVS), pp. 451–460.

LICS-2012-MullerT #random

Short Propositional Refutations for Dense Random 3CNF Formulas (SM, IT), pp. 501–510.

SAT-2012-AchlioptasM #algorithm #bound #exponential #random #satisfiability

Exponential Lower Bounds for DPLL Algorithms on Satisfiable Random 3-CNF Formulas (DA, RMM), pp. 327–340.

SAT-2012-AnsoteguiGL #community #satisfiability

The Community Structure of SAT Formulas (CA, JGC, JL), pp. 410–423.

SAT-2012-BalabanovCJ #quantifier

Henkin Quantifiers and Boolean Formulae (VB, HJKC, JHRJ), pp. 129–142.

SAT-2012-GelderWL #preprocessor #quantifier

Extended Failed-Literal Preprocessing for Quantified Boolean Formulas (AVG, SBW, FL), pp. 86–99.

TAP-2012-CreignouES #framework #random #satisfiability #specification

A Framework for the Specification of Random SAT and QSAT Formulas (NC, UE, MS), pp. 163–168.

VMCAI-2012-SackZ #framework #probability

A General Framework for Probabilistic Characterizing Formulae (JS, LZ), pp. 396–411.

ICDAR-2011-CelikY #2d #graph grammar #probability #recognition #using

Probabilistic Mathematical Formula Recognition Using a 2D Context-Free Graph Grammar (MC, BAY), pp. 161–166.

ICDAR-2011-LinGTLH #documentation #identification

Mathematical Formula Identification in PDF Documents (XL, LG, ZT, XL, XH), pp. 1419–1423.

ICALP-v2-2011-BovaCV #comparison

Generic Expression Hardness Results for Primitive Positive Formula Comparison (SB, HC, MV), pp. 344–355.

ICFP-2011-Chargueraud #imperative #source code #verification

Characteristic formulae for the verification of imperative programs (AC), pp. 418–430.

CSL-2011-CardelliLM #axiom #logic #markov #metric

Continuous Markovian Logic — From Complete Axiomatization to the Metric Space of Formulas (LC, KGL, RM), pp. 144–158.

SAT-2011-OrdyniakPS #satisfiability

Satisfiability of Acyclic and almost Acyclic CNF Formulas (II) (SO, DP, SS), pp. 47–60.

CASE-2010-KumarKST #predict #programming

A mathematical programming for predicting molecular formulas in accurate mass spectrometry (SK, MK, RS, KT), pp. 246–251.

SAS-2010-BrauerK #abstraction #automation #using

Automatic Abstraction for Intervals Using Boolean Formulae (JB, AK), pp. 167–183.

SAS-2010-DilligDA #constraints #online #scalability #source code #static analysis

Small Formulas for Large Programs: On-Line Constraint Simplification in Scalable Static Analysis (ID, TD, AA), pp. 236–252.

STOC-2010-Raz #bound

Tensor-rank and lower bounds for arithmetic formulas (RR), pp. 659–666.

ICALP-v1-2010-BhattacharyaDMT #approximate #on the

On Approximate Horn Formula Minimization (AB, BD, DM, GT), pp. 438–450.

ICFP-2010-Chargueraud #verification

Program verification through characteristic formulae (AC), pp. 321–332.

KR-2010-BartholomewL #decidability #modelling

A Decidable Class of Groundable Formulas in the General Theory of Stable Models (MB, JL).

ICLP-J-2010-WangYYS #logic programming #source code

Loop formulas for description logic programs (YW, JHY, LYY, YDS), pp. 531–545.

IJCAR-2010-BlanchetteK #higher-order

Monotonicity Inference for Higher-Order Formulas (JCB, AK), pp. 91–106.

SAT-2010-Ben-SassonJ #bound #learning #strict

Lower Bounds for Width-Restricted Clause Learning on Small Width Formulas (EBS, JJ), pp. 16–29.

SAT-2010-NamasivayamT

Simple but Hard Mixed Horn Formulas (GN, MT), pp. 382–387.

DAC-2009-JainC #graph #performance #satisfiability #using

Efficient SAT solving for non-clausal formulas using DPLL, graphs, and watched cuts (HJ, EMC), pp. 563–568.

ICDAR-2009-WangSY #comprehension #online

The Understanding and Structure Analyzing for Online Handwritten Chemical Formulas (XW, GS, JY), pp. 1056–1060.

ICALP-v1-2009-Morizumi

Limiting Negations in Formulas (HM), pp. 701–712.

ICALP-v2-2009-BlumensathOW #bound #finite #higher-order #monad #word

Boundedness of Monadic Second-Order Formulae over Finite Words (AB, MO, MW), pp. 67–78.

ICALP-v2-2009-MelliesTT #exponential #linear #logic

An Explicit Formula for the Free Exponential Modality of Linear Logic (PAM, NT, CT), pp. 247–260.

IFM-2009-VargasGTG #ltl #model checking

Model Checking LTL Formulae in RAISE with FDR (APV, AGG, SLTT, CG), pp. 231–245.

HIMI-DIE-2009-HijikataHN

Search Mathematical Formulas by Mathematical Formulas (YH, HH, SN), pp. 404–411.

PPDP-2009-Aranda-LopezNSS #constraints #database #deduction #fixpoint #implementation #semantics

Implementing a fixed point semantics for a constraint deductive database based on hereditary harrop formulas (GAL, SN, FSP, JSH), pp. 117–128.

CAV-2009-GeM #modulo theories #quantifier #satisfiability

Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories (YG, LMdM), pp. 306–320.

CSL-2009-AdlerW #first-order

Tree-Width for First Order Formulae (IA, MW), pp. 71–85.

SAT-2009-BuningZB #quantifier #subclass

Resolution and Expressiveness of Subclasses of Quantified Boolean Formulas and Circuits (HKB, XZ, UB), pp. 391–397.

SAT-2009-JohannsenRW #satisfiability #strict

Solving SAT for CNF Formulas with a One-Sided Restriction on Variable Occurrences (DJ, IR, MW), pp. 80–85.

SAT-2009-PorschenSS #aspect-oriented #on the

On Some Aspects of Mixed Horn Formulas (SP, TS, ES), pp. 86–100.

CASE-2008-Chirikjian

Parts entropy and the principal kinematic formula (GSC), pp. 864–869.

DAC-2008-ChenLC #predict

Predictive formulae for OPC with applications to lithography-friendly routing (TCC, GWL, YWC), pp. 510–515.

STOC-2008-ReichardtS #algorithm #quantum

Span-program-based quantum algorithm for evaluating formulas (BR, RS), pp. 103–112.

FLOPS-2008-NievaSS #constraints #database #deduction #formal method

Formalizing a Constraint Deductive Database Language Based on Hereditary Harrop Formulas with Negation (SN, JSH, FSP), pp. 289–304.

ICALP-A-2008-BuchfuhrerU #complexity

The Complexity of Boolean Formula Minimization (DB, CU), pp. 24–35.

GT-VMT-2008-BottoniMWY #control flow

Composing control flow and formula rules for computing on grids (PB, NNM, YW, RY).

KR-2008-LeeM #on the

On Loop Formulas with Variables (JL, YM), pp. 444–453.

SAC-2008-BelohlavekV #concept analysis #dependence

Adding background knowledge to formal concept analysis via attribute dependency formulas (RB, VV), pp. 938–943.

ICLP-2008-LeeLP #modelling

Safe Formulas in the General Theory of Stable Models (Preliminary Report) (JL, VL, RP), pp. 672–676.

SAT-2008-CreignouDER #quantifier #random

New Results on the Phase Transition for Random Quantified Boolean Formulas (NC, HD, UE, RR), pp. 34–47.

SAT-2008-PorschenS #linear

A CNF Class Generalizing Exact Linear Formulas (SP, ES), pp. 231–245.

ICDAR-2007-ChangTO #image #physics #segmentation

Physical Structure Segmentation with Projection Profile for Mathematic Formulae and Graphics in Academic Paper Images (TYC, YT, MO), pp. 1193–1197.

ICDAR-2007-PrusaH #2d #recognition #using

Mathematical Formulae Recognition Using 2D Grammars (DP, VH), pp. 849–853.

TACAS-2007-CondratK #approach #preprocessor

A Gröbner Basis Approach to CNF-Formulae Preprocessing (CC, PK), pp. 618–631.

TACAS-2007-TsayCTWC #automaton #named #visual notation

GOAL: A Graphical Tool for Manipulating Büchi Automata and Temporal Formulae (YKT, YFC, MHT, KNW, WCC), pp. 466–471.

ICALP-2007-DawarGKS #scalability

Model Theory Makes Formulas Large (AD, MG, SK, NS), pp. 913–924.

SEKE-2007-SalamahKG #generative #linear #logic #specification

Generating Linear Temporal Logic Formulas for Pattern-Based Specifications (SS, VK, AQG), pp. 422–427.

SAC-2007-Dufourd #framework #proving #theorem

A hypermap framework for computer-aided proofs in surface subdivisions: genus theorem and Euler’s formula (JFD), pp. 757–761.

CADE-2007-Aderhold

Improvements in Formula Generalization (MA), pp. 231–246.

SAT-2007-AudemardS #encoding

Circuit Based Encoding of CNF Formula (GA, LS), pp. 16–21.

SAT-2007-SamerS #quantifier #set

Backdoor Sets of Quantified Boolean Formulas (MS, SS), pp. 230–243.

SAT-2007-Szeider #set

Matched Formulas and Backdoor Sets (SS), pp. 94–99.

ICPR-v2-2006-TakiguchiOM #case study #comprehension #fault #recognition

A Study on Character Recognition Error Correction at Higher Level Recognition Step for Mathematical Formulae Understanding (YT, MO, YM), pp. 966–969.

KR-2006-ChenLWZ #first-order #logic programming #source code

First-Order Loop Formulas for Normal Logic Programs (YC, FL, YW, MZ), pp. 298–307.

KR-2006-ChevaleyreEL #modelling #power of

Expressive Power of Weighted Propositional Formulas for Cardinal Preference Modeling (YC, UE, JL), pp. 145–152.

KR-2006-Coste-MarquisFLBM #policy #quantifier #representation

Representing Policies for Quantified Boolean Formulae (SCM, HF, JL, DLB, PM), pp. 286–297.

ICSE-2006-JorgesMS #generative #graph #modelling #named

FormulaBuilder: a tool for graph-based modelling and generation of formulae (SJ, TMS, BS), pp. 815–818.

IJCAR-2006-ReeberH #satisfiability #subclass

A SAT-Based Decision Procedure for the Subclass of Unrollable List Formulas in ACL2 (SULFA) (ER, WAHJ), pp. 453–467.

LICS-2006-ChaubardPS #composition #first-order

First Order Formulas with Modular Predicates (LC, JÉP, HS), pp. 211–220.

SAT-2006-BubeckB #complexity #dependence #modelling #quantifier

Dependency Quantified Horn Formulas: Models and Complexity (UB, HKB), pp. 198–211.

SAT-2006-BuningZ #quantifier

Minimal False Quantified Boolean Formulas (HKB, XZ), pp. 339–352.

SAT-2006-DantsinW #constant #performance #satisfiability

MAX-SAT for Formulas with Constant Clause Density Can Be Solved Faster Than in O(s2) Time (ED, AW), pp. 266–276.

SAT-2006-JainBC #satisfiability #using

Satisfiability Checking of Non-clausal Formulas Using General Matings (HJ, CB, EMC), pp. 75–89.

SAT-2006-PorschenSR #linear #on the

On Linear CNF Formulas (SP, ES, BR), pp. 212–225.

SAT-2006-TangM #quantifier

Solving Quantified Boolean Formulas with Circuit Observability Don’t Cares (DT, SM), pp. 368–381.

ICDAR-2005-TakiguchiOM #comprehension #layout #recognition #semantics

A Fundamental Study of Output Translation from Layout Recognition and Semantic Understanding System for Mathematical Formulae (YT, MO, YM), pp. 745–749.

CIAA-2005-KleinB #automaton #linear #logic

Experiments with Deterministic ω-Automata for Formulas of Linear Temporal Logic (JK, CB), pp. 199–212.

ICALP-2005-HanedaKT

Suitable Curves for Genus-4 HCC over Prime Fields: Point Counting Formulae for Hyperelliptic Curves of Type y2=x2k+1+ax (MH, MK, TT), pp. 539–550.

LOPSTR-2005-PettorossiPS #array #protocol #using #verification

Transformational Verification of Parameterized Protocols Using Array Formulas (AP, MP, VS), pp. 23–43.

SPLC-2005-Batory #feature model #modelling

Feature Models, Grammars, and Propositional Formulas (DSB), pp. 7–20.

SAT-J-2004-BuningZ05 #equivalence #modelling #quantifier

Equivalence Models for Quantified Boolean Formulas (HKB, XZ), pp. 224–234.

SAT-J-2004-ChenD05 #algebra #quantifier

Looking Algebraically at Tractable Quantified Boolean Formulas (HC, VD), pp. 71–79.

SAT-J-2004-JiaMS05 #satisfiability

From Spin Glasses to Hard Satisfiable Formulas (HJ, CM, BS), pp. 199–210.

SAT-J-2004-TangYRM05 #algorithm #analysis #problem #quantifier #satisfiability

Analysis of Search Based Algorithms for Satisfiability of Propositional and Quantified Boolean Formulas Arising from Circuit State Space Diameter Problems (DT, YY, DR, SM), pp. 292–305.

LICS-2005-Atserias05a #random

Definability on a Random 3-CNF Formula (AA), pp. 458–466.

SAT-2005-AudemardS #approach #quantifier

A Symbolic Search Based Approach for Quantified Boolean Formulas (GA, LS), pp. 16–30.

SAT-2005-BubeckBZ #equivalence #modelling #quantifier

Quantifier Rewriting and Equivalence Models for Quantified Horn Formulas (UB, HKB, XZ), pp. 386–392.

SAT-2005-Coste-MarquisBL #branch #heuristic #quantifier

A Branching Heuristics for Quantified Renamable Horn Formulas (SCM, DLB, FL), pp. 393–399.

SAT-2005-GershmanS #effectiveness #preprocessor

Cost-Effective Hyper-Resolution for Preprocessing CNF Formulas (RG, OS), pp. 423–429.

SAT-2005-MarinovKBZR #compilation #declarative #modelling #optimisation

Optimizations for Compiling Declarative Models into Boolean Formulas (DM, SK, SB, LZ, MCR), pp. 187–202.

SAT-2005-MneimnehLASS #algorithm #bound #satisfiability

A Branch-and-Bound Algorithm for Extracting Smallest Minimal Unsatisfiable Formulas (MNM, IL, ZSA, JPMS, KAS), pp. 467–474.

SAT-2005-Wahlstrom #performance #satisfiability

Faster Exact Solving of SAT Formulae with a Low Number of Occurrences per Variable (MW), pp. 309–323.

STOC-2004-Aaronson #multi #quantum

Multilinear formulas and skepticism of quantum computing (SA), pp. 118–127.

STOC-2004-Raz #multi

Multi-linear formulas for permanent and determinant are of super-polynomial size (RR), pp. 633–641.

ICALP-2004-AlekhnovichHI #algorithm #bound #exponential #satisfiability

Exponential Lower Bounds for the Running Time of DPLL Algorithms on Satisfiable Formulas (MA, EAH, DI), pp. 84–96.

ICALP-2004-FeigeO #random #scalability

Easily Refutable Subformulas of Large Random 3CNF Formulas (UF, EO), pp. 519–530.

ICALP-2004-Skelley #quantifier #reasoning #source code

Propositional PSPACE Reasoning with Boolean Programs Versus Quantified Boolean Formulas (AS), pp. 1163–1175.

ICPR-v2-2004-ToyozumiYMKMST #case study #recognition #segmentation #using

A Study of Symbol Segmentation Method for Handwritten Mathematical Formula Recognition using Mathematical Structure Information (KT, NY, KM, TK, KM, YS, TT), pp. 630–633.

KR-2004-Davis #communication #first-order

A First-Order Theory of Communicating First-Order Formulas (ED), pp. 235–245.

CC-2004-ParkerC #algorithm

An Automata-Theoretic Algorithm for Counting Solutions to Presburger Formulas (EP, SC), pp. 104–119.

LICS-2004-Latour #automaton #integer

From Automata to Formulas: Convex Integer Polyhedra (LL), pp. 120–129.

LICS-2004-SeshiaB #bound #quantifier #using

Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds (SAS, REB), pp. 100–109.

SAT-2004-BuningZ #equivalence #modelling #quantifier

Equivalence Models for Quantified Boolean Formulas (HKB, XZ), pp. 230–237.

SAT-2004-ChenD #algebra #quantifier

Looking Algebraically at Tractable Quantified Boolean Formulas (HC, VD), pp. 224–229.

SAT-2004-JiaMS #satisfiability

From Spin Glasses to Hard Satisfiable Formulas (HJ, CM, BS), pp. 12–19.

SAT-2004-Stachniak

A Note on Satisfying Truth-Value Assignments of Boolean Formulas (ZS), pp. 104–110.

SAT-2004-TangYRM #algorithm #analysis #problem #quantifier #satisfiability

Analysis of Search Based Algorithms for Satisfiability of Quantified Boolean Formulas Arising from Circuit State Space Diameter Problems (DT, YY, DR, SM), pp. 214–223.

SAT-2004-ThiffaultBW

Solving Non-clausal Formulas with DPLL search (CT, FB, TW), pp. 147–156.

DATE-2003-ChenHBW #automation #constraints #generative #monitoring #simulation

Automatic Generation of Simulation Monitors from Quantitative Constraint Formula (XC, HH, FB, YW), pp. 11174–11175.

DATE-2003-GoldbergN #proving #satisfiability #verification

Verification of Proofs of Unsatisfiability for CNF Formulas (EIG, YN), pp. 10886–10891.

ICDAR-2003-JinHW

Mathematical Formulas Extraction (JJ, XH, QW), pp. 1138–1141.

ICDAR-2003-TapiaR #online #recognition

Recognition of On-line Handwritten Mathematical Formulas in the E-Chalk System (ET, RR), pp. 980–984.

ESOP-2003-RepsSL #difference #finite #logic #static analysis

Finite Differencing of Logical Formulas for Static Analysis (TWR, SS, AL), pp. 380–398.

CADE-2003-SchmidtH #axiom #first-order

A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae (RAS, UH), pp. 412–426.

ICLP-2003-LeeL #logic programming #source code

Loop Formulas for Disjunctive Logic Programs (JL, VL), pp. 451–465.

LICS-2003-GurevichS #higher-order #monad

Spectra of Monadic Second-Order Formulas with One Unary Function (YG, SS), pp. 291–300.

SAT-2003-BuningSZ #modelling #on the #quantifier

On Boolean Models for Quantified Boolean Horn Formulas (HKB, KS, XZ), pp. 93–104.

SAT-2003-DequenD #named #performance #random #satisfiability

kcnfs: An Efficient Solver for Random k-SAT Formulae (GD, OD), pp. 486–501.

SAT-2003-EglySTWZ #quantifier

Comparing Different Prenexing Strategies for Quantified Boolean Formulas (UE, MS, HT, SW, MZ), pp. 214–228.

SAT-2003-HanataniHI

Density Condensation of Boolean Formulas (YH, TH, KI), pp. 69–77.

SAT-2003-MaarenN

Hidden Threshold Phenomena for Fixed-Density SAT-formulae (HvM, LvN), pp. 135–149.

SAT-2003-Williams #on the

On Computing k-CNF Formula Properties (RW), pp. 330–340.

SAS-2002-GallardoMP #ltl #model checking #refinement

Refinement of LTL Formulas for Abstract Model Checking (MdMG, PM, EP), pp. 395–410.

STOC-2002-HellersteinR #learning #using

Exact learning of DNF formulas using DNF hypotheses (LH, VR), pp. 465–473.

CADE-2002-AudemardBCKS #approach #linear #satisfiability

A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions (GA, PB, AC, AK, RS), pp. 195–210.

CADE-2002-Goldberg #satisfiability #testing

Testing Satisfiability of CNF Formulas by Computing a Stable Set of Points (EG), pp. 161–180.

CAV-2002-BarrettDS #first-order #incremental #satisfiability

Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT (CWB, DLD, AS), pp. 236–249.

CAV-2002-PurandareS

Vacuum Cleaning CTL Formulae (MP, FS), pp. 485–499.

CAV-2002-StrichmanSB #satisfiability

Deciding Separation Formulas with SAT (OS, SAS, REB), pp. 209–222.

CSL-2002-ChernovSSV #logic

Variants of Realizability for Propositional Formulas and the Logic of the Weak Law of Excluded Middle (AVC, DPS, EZS, NKV), pp. 74–88.

LICS-2002-Atserias #random #satisfiability

Unsatisfiable Random Formulas Are Hard to Certify (AA), pp. 325–334.

LICS-2002-RepsLS #semantics

Semantic Minimization of 3-Valued Propositional Formulae (TWR, AL, SS), p. 40–?.

RTA-2002-DeharbeMR #logic #model checking

Improving Symbolic Model Checking by Rewriting Temporal Logic Formulae (DD, AMM, CR), pp. 207–221.

SAT-2002-Bruni #satisfiability

Exact selection of minimal unsatisfiable subformulae for special classes of propositional formulae (RB), p. 22.

SAT-2002-BueningX #complexity #morphism #satisfiability

The complexity of homomorphisms and renamings of minimal unsatisfiable formulas (HKB, DX), p. 9.

SAT-2002-DuboisD #random #satisfiability

Renormalization as a function of clause lengths for solving random k-SAT formulae (OD, GD), p. 15.

SAT-2002-Goldberg #satisfiability #testing

Testing satisfiability of CNF formulas by computing a stable set of points (EG), p. 12.

SAT-2002-ManyaABCL

Resolution methods for many-valued CNF formulas (FM, CA, RB, AC, CML), p. 42.

SAT-2002-MatsuuraI

Inclusion-exclusion for k-CNF formulas (AM, KI), p. 3.

SAT-2002-Szeider

Generalizations of matched CNF formulas (SS), p. 7.

SAT-2002-ZhaoB #equivalence #problem

Extension and equivalence problems for clause minimal formulas (XZ, HKB), p. 43.

DATE-2001-YuK #algorithm #distributed #performance

Explicit formulas and efficient algorithm for moment computation of coupled RC trees with lumped and distributed elements (QY, ESK), pp. 445–450.

ICDAR-2001-Couasnon #automation #documentation #generative #named #recognition

DMOS: A Generic Document Recognition Method, Application to an Automatic Generator of Musical Scores, Mathematical Formulae and Table Structures Recognition Systems (BC), pp. 215–220.

ICDAR-2001-EtoS #network #recognition #using

Mathematical Formula Recognition Using Virtual Link Network (YE, MS), pp. 762–767.

ICDAR-2001-ToyozumiMSS #realtime #recognition

A System for Real-time Recognition of Handwritten Mathematical Formulas (KT, KM, YS, TS), pp. 1059–1063.

FLOPS-2001-Delzanno #case study #debugging #prolog #protocol #security #specification

Specifying and Debugging Security Protocols via Hereditary Harrop Formulas and λ Prolog — A Case-study (GD), pp. 123–137.

CAV-2001-AsterothBA #model checking #modelling

Model Checking with Formula-Dependent Abstract Models (AA, CB, UA), pp. 155–168.

IJCAR-2001-GiunchigliaNT #named #quantifier #satisfiability

QUBE: A System for Deciding Quantified Boolean Formulas Satisfiability (EG, MN, AT), pp. 364–369.

IJCAR-2001-Patel-SchneiderS #generative #random

A New System and Methodology for Generating Random Modal Formulae (PFPS, RS), pp. 464–468.

LICS-2001-AdlerI #bound #exclamation

An n! Lower Bound on Formula Size (MA, NI), pp. 197–206.

SAT-2001-BuningZ #satisfiability

Satisfiable Formulas Closed Under Replacement (HKB, XZ), pp. 48–58.

ICALP-2000-Pichler #equation

Negation Elimination from Simple Equational Formulae (RP), pp. 612–623.

ICML-2000-SingerV #learning #modelling #performance #predict

Learning to Predict Performance from Formula Modeling and Training Data (BS, MMV), pp. 887–894.

ICPR-v1-2000-KacemBA #embedded

Embedded Formulas Extraction (AK, AB, MBA), pp. 1676–1680.

ICPR-v2-2000-KosmalaRB #execution #online #recognition

On-Line Handwritten Formula Recognition with Integrated Correction Recognition and Execution (AK, GR, AB), pp. 2590–2593.

ICPR-v4-2000-SuzukiMSA #realtime #recognition

A New System for the Real-Time Recognition of Handwritten Mathematical Formulas (TS, KM, YS, SA), pp. 4515–4518.

CAV-2000-SomenziB #automaton #ltl #performance

Efficient Büchi Automata from LTL Formulae (FS, RB), pp. 248–263.

CL-2000-AltamiranoE

Finding Tractable Formulas in NNF (EA, GEI), pp. 493–507.

CL-2000-Dierkes

An Application of Model Building in a Resolution Decision Procedure for Guarded Formulas (MD), pp. 583–597.

CL-2000-MoinardR #finite #set

Smallest Equivalent Sets for Finite Propositional Formula Circumscription (YM, RR), pp. 897–911.

CL-2000-PearceGV #equilibrium #modelling #using

Computing Equilibrium Models Using Signed Formulas (DP, IPdG, AV), pp. 688–702.

CSL-2000-Atserias #bound #complexity #fixpoint

The Descriptive Complexity of the Fixed-Points of Bounded Formulas (AA), pp. 172–186.

ICDAR-1999-KosmalaRLP #graph grammar #markov #modelling #online #recognition #using

On-Line Handwritten Formula Recognition using Hidden Markov Models and Context Dependent Graph Grammars (AK, GR, SL, LP), pp. 107–110.

ICDAR-1999-RamelBE #automation #image #representation

Automatic Reading of Handwritten Chemical Formulas from a Structural Representation of the Image (JYR, GB, HE), pp. 83–86.

FM-v1-1999-BarbutiFSV #abstraction #model checking #realtime

Formula Based Abstractions of Transition Systems for Real-Time Model Checking (RB, NDF, AS, GV), pp. 289–306.

SIGIR-1999-DaiLK #information management #segmentation #statistics

A New Statistical Formula for Chinese Text Segmentation Incorporating Contextual Information (YD, TEL, CSGK), pp. 82–89.

CAV-1999-PnueliRSS #similarity

Deciding Equality Formulas by Small Domains Instantiations (AP, YR, OS, MS), pp. 455–469.

RTA-1999-CaronSTT #quantifier #satisfiability

Deciding the Satisfiability of Quantifier free Formulae on One-Step Rewriting (ACC, FS, ST, MT), pp. 103–117.

RTA-1999-Courcelle #graph #logic

Hierarchical Graph Decompositions Defined by Grammars and Logical Formulas (BC), pp. 90–91.

DAC-1998-AmonBL #using

Making Complex Timing Relationships Readable: Presburger Formula Simplicication Using Don’t Cares (TA, GB, JL), pp. 586–590.

STOC-1998-BeameKPS #complexity #on the #proving #random #satisfiability

On the Complexity of Unsatisfiability Proofs for Random k-CNF Formulas (PB, RMK, TP, MES), pp. 561–571.

TAGT-1998-BottoniPS #term rewriting

From Formulae to Rewriting Systems (PB, FPP, MS), pp. 267–280.

AdaEurope-1998-Chapront #ada #development #safety

Ada+B The Formula for Safety Critical Software Development (PC), pp. 13–18.

ICPR-1998-KosmalaR #online #recognition #statistics #using

On-line handwritten formula recognition using statistical methods (AK, GR), pp. 1306–1308.

CAV-1998-BeerBL #model checking #on the fly

On-the-Fly Model Checking of RCTL Formulas (IB, SBD, AL), pp. 184–194.

DAC-1997-AmonBHL #diagrams #using #verification

Symbolic Timing Verification of Timing Diagrams using Presburger Formulas (TA, GB, TH, JL), pp. 226–231.

ICDAR-1997-Lavirotte #recognition

Optical Formula Recognition (SL), pp. 357–361.

ILPS-1997-LeachNR #constraints #logic programming

Constraint Logic Programming with Hereditary Harrop Formulas (JL, SN, MRA), pp. 307–321.

STOC-1996-BergadanoCV #learning #query

Learning Sat-k-DNF Formulas from Membership Queries (FB, DC, SV), pp. 126–130.

STOC-1996-Bshouty #towards

Towards the Learnability of DNF Formulae (NHB), pp. 131–140.

STOC-1996-Fu #composition #proving

Modular Coloring Formulas Are Hard for Cutting Planes Proofs (XF), pp. 595–602.

KR-1996-Morgenstern #network #semantics

Inheriting Well-formed Formulae in a Formula-Agumented Semantic Network (LM), pp. 268–279.

CADE-1996-ParkG #clustering #satisfiability #scalability #testing

Partitioning Methods for Satisfiability Testing on Large Formulas (TJP, AVG), pp. 748–762.

CSL-1996-Setzer #decidability #induction

Inductive Definitions with Decidable Atomic Formulas (AS), pp. 414–430.

TACAS-1995-EngbergL #bisimulation #performance

Efficient Simplification of Bisimulation Formulas (UE, KSL), pp. 111–132.

ILPS-1995-Hui-Bon-Hoa #proving

Clause-based proofs for hereditary Harrop formulas (AHBH), pp. 179–193.

PLDI-1994-Pugh #how #why

Counting Solutions to Presburger Formulas: How and Why (WP), pp. 121–134.

CADE-1994-ChazarainK #induction #proving

Mechanizable Inductive Proofs for a Class of Forall Exists Formulas (JC, EK), pp. 118–132.

CAV-1994-AzizSS #composition #equivalence #model checking

Formula-Dependent Equivalence for Compositional CTL Model Checking (AA, TRS, VS), pp. 324–337.

HCI-ACS-1993-Lewis #modelling #probability #problem #usability

Problem Discovery in Usability Studies: A Models Based on the Binomial Probability Formula (JRL), pp. 666–671.

RTA-1993-Tajine #decidability #equation

The Negation Elimination from Syntactic Equational Formula is Decidable (MT), pp. 316–327.

STOC-1992-BlumR #learning #performance #query

Fast Learning of k-Term DNF Formulas with Queries (AB, SR), pp. 382–389.

STOC-1992-BshoutyHH #learning

Learning Arithmetic Read-Once Formulas (NHB, TRH, LH), pp. 370–381.

ICALP-1992-Straubing #complexity #first-order #power of

Circuit Complexity and the Expressive Power of Generalized First-Order Formulas (HS), pp. 16–27.

CADE-1992-Fisher #first-order #normalisation

A Normal Form for First-Order Temporal Formulae (MF), pp. 370–384.

ICALP-1991-Fouks

General Resolution of Tseitin Formulas is Hard (JDF), pp. 151–162.

LOPSTR-1991-Noel #nondeterminism

A Method for the Determinisation of Propositional Temporal Formulae (PN), pp. 276–296.

CAV-1991-Korver #bisimulation #branch

Computing Distinguishing Formulas for Branching Bisimulation (HK), pp. 13–23.

CSL-1991-Dahlhaus #first-order #how #memory management #modelling

How to Implement First Order Formulas in Local Memory Machine Models (ED), pp. 68–78.

LICS-1991-CortesiFW #abstract domain #analysis

Prop revisited: Propositional Formula as Abstract Domain for Groundness Analysis (AC, GF, WHW), pp. 322–327.

STOC-1990-Cleve #bound #simulation #source code #towards

Towards Optimal Simulations of Formulas by Bounded-Width Programs (RC), pp. 271–277.

ICALP-1990-Comon #algebra #equation #order

Equational Formulas in Order-Sorted Algebras (HC), pp. 674–688.

POPL-1990-AspertiFG #proving

Implicative Formulae in the “Proofs as Computations” Analogy (AA, GLF, RG), pp. 59–71.

POPL-1990-Griffin #type system

A Formulae-as-Types Notion of Control (TG), pp. 47–58.

CSL-1990-FlogelKB #quantifier #subclass

Subclasses of Quantified Boolean Formulas (AF, MK, HKB), pp. 145–155.

STOC-1989-KearnsV #automaton #encryption #finite #learning

Cryptographic Limitations on Learning Boolean Formulae and Finite Automata (MJK, LGV), pp. 433–444.

ICALP-1989-Steffen

Characteristic Formulae (BS), pp. 723–732.

CHI-1989-Nakayama #editing

Mathematical formula editor for CAI (YN), pp. 387–392.

CSL-1989-Mundici

Reducibility of Monotone Formulas to μ-Formulas (DM), pp. 267–270.

SIGMOD-1988-YounHH #classification #database #deduction #recursion

Classification of Recursive Formulas in Deductive Databases (CY, LJH, JH), pp. 320–328.

STOC-1988-Ben-OrC #algebra #constant #using

Computing Algebraic Formulas Using a Constant Number of Registers (MBO, RC), pp. 254–257.

ICALP-1988-KuceraMP #on the

On the Learnability of DNF Formulae (LK, AMS, MP), pp. 347–361.

CADE-1988-Moser #graph

A Decision Procedure for Unquantified Formulas of Graph Theory (LEM), pp. 344–357.

CSL-1988-Schatz

Delete Operations and Horn Formulas (RS), pp. 329–343.

PODS-1987-GelderT #calculus #relational #safety

Safety and Correct Translation of Relational Calculus Formulas (AVG, RWT), pp. 313–327.

STOC-1987-Buss #problem

The Boolean Formula Value Problem Is in ALOGTIME (SRB), pp. 123–131.

STOC-1987-KearnsLPV #on the

On the Learnability of Boolean Formulae (MJK, ML, LP, LGV), pp. 285–295.

ICALP-1987-Josko #liveness #model checking

Modelchecking of CTL Formulae under Liveness Assumptions (BJ), pp. 280–289.

CSL-1987-Lowen #aspect-oriented #logic #optimisation

Optimization Aspects of Logical Formulas (UL), pp. 173–187.

CSL-1987-Schoning #complexity

Complexity Cores and Hard-To-Prove Formulas (US), pp. 273–280.

LICS-1987-MillerNS #proving

Hereditary Harrop Formulas and Uniform Proof Systems (DM, GN, AS), pp. 98–105.

SLP-1987-MillerN87 #approach #logic programming #source code

A Logic Programming Approach to Manipulating Formulas and Programs (DM, GN), pp. 379–388.

CADE-1986-BuningL #first-order #satisfiability

Classes of First Order Formulas Under Various Satisfiability Definitions (HKB, TL), pp. 553–563.

CADE-1986-KanamoriF #induction #prolog #source code #verification

Formulation of Induction Formulas in Verification of Prolog Programs (TK, HF), pp. 281–299.

CADE-1986-Lins #combinator #execution

A New Formula for the Execution of Categorial Combinators (RDL), pp. 89–98.

CADE-1986-Weispfenning #logic #recursion #source code

Diamond Formulas in the Dynamic Logic of Recursively Enumerable Programs (VW), pp. 564–571.

STOC-1984-KlawePPY #on the #strict

On Monotone Formulae with Restricted Depth (Preliminary Version) (MMK, WJP, NP, MY), pp. 480–487.

SLP-1984-GergelyS84 #logic programming

Cuttable Formulas for Logic Programming (TG, MS), pp. 299–310.

ICALP-1982-Kalorkoti #bound

A Lower Bound for the Formula Size of Rational Functions (KK), pp. 330–338.

STOC-1980-Plaisted #independence #on the

On the Distribution of Independent Formulae of Number Theory (DAP), pp. 39–44.

ICALP-1980-Snir #complexity #on the

On the Size Complexity of Monotone Formulas (MS), pp. 621–631.

CADE-1980-LovelandS

Simplifying Interpreted Formulas (DWL, RES), pp. 97–109.

ICALP-1978-Commentz-Walter #trade-off

Size-Depth Tradeoff in Boolean Formulas (BCW), pp. 125–141.

GG-1978-EhrigL #graph grammar #parallel

Locally Star Sluing Formulas for a Class of Parallel Graph Grammars (HE, AL), pp. 206–223.

STOC-1975-FischerMP #bound

Lower Bounds on the Size of Boolean Formulas: Preliminary Report (MJF, ARM, MP), pp. 37–44.

STOC-1972-JonesS #first-order #similarity #turing machine

Turing Machines and the Spectra of First-Order Formulas with Equality (NDJ, ALS), pp. 157–167.

SIGIR-1971-Paola #problem #relational

The Relational Data File and the Decision Problem for Classes of Proper Formulas (RADP), pp. 95–104.