Repository logo

Infoscience

  • English
  • French
Log In
Logo EPFL, École polytechnique fédérale de Lausanne

Infoscience

  • English
  • French
Log In
  1. Home
  2. Academic and Research Output
  3. Reports, Documentation, and Standards
  4. On Locality of One-Variable Axioms and Piecewise Combinations
 
report

On Locality of One-Variable Axioms and Piecewise Combinations

Jacobs, Swen
•
Kuncak, Viktor  orcid-logo
2010

Local theory extensions provide a complete and efficient way for reasoning about satisfiability of certain kinds of universally quantified formulas modulo a background theory. They are therefore useful in automated reasoning, software verification, and synthesis. In this paper, we 1) provide a sufficient condition for locality of axioms with one variable specifying functions and relations, 2) show how to obtain local axiomatizations from non-local ones in some cases, 3) show how to obtain piecewise combination of different local theory extensions.

  • Files
  • Details
  • Metrics
Loading...
Thumbnail Image
Name

JacobsKuncak-OneVariable.pdf

Access type

openaccess

Size

263.81 KB

Format

Adobe PDF

Checksum (MD5)

91a6b99db03175c05a5f0d5ef00a44ae

Logo EPFL, École polytechnique fédérale de Lausanne
  • Contact
  • infoscience@epfl.ch

  • Follow us on Facebook
  • Follow us on Instagram
  • Follow us on LinkedIn
  • Follow us on X
  • Follow us on Youtube
AccessibilityLegal noticePrivacy policyCookie settingsEnd User AgreementGet helpFeedback

Infoscience is a service managed and provided by the Library and IT Services of EPFL. © EPFL, tous droits réservés